An interleaving symbolic execution approach for the formal verification of Ada programs with tasking

6 January 2003

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

p. 15-26
https://doi.org/10.1109/ada.1988.4781

Abstract

The use of symbolic execution to prove partial correctness and general safety properties of Ada programs is considered. Past efforts are extended by incorporating tasking proof rules into the symbolic executor, allowing Ada programs with tasking to be formally verified.<>

Keywords

INTERLEAVED CODES
FORMAL VERIFICATION
TESTING
SAFETY
COMPUTER SCIENCE
SEQUENTIAL ANALYSIS
DATA STRUCTURES
DELAY EFFECTS

This publication has 0 references indexed in Scilit: