DocumentCode
2695716
Title
Symbolic execution-based verification of Ada tasking programs
Author
Dillon, Laura K.
Author_Institution
Dept. of Comput. Sci., California Univ., Santa Barbara, CA, USA
fYear
1988
fDate
23-25 May 1988
Firstpage
3
Lastpage
13
Abstract
Symbolic execution has been used successfully with sequential programs for generating the verification conditions required for correctness proofs. It is shown how the symbolic execution model for sequential programs can be extended to a tasking subset of Ada. The criteria for correct operation of a concurrent program include safety properties, such as mutual exclusion and freedom from deadlock. The extended model, therefore, provides a basis for the automatic generation of verification conditions for proving general safety properties of Ada tasking programs
Keywords
Ada; parallel programming; program verification; symbol manipulation; Ada tasking programs; automatic generation; concurrent program; correctness proofs; mutual exclusion; safety properties; sequential programs; symbolic execution model; tasking subset; verification conditions; Computer science; Interleaved codes; Logic; Safety; System recovery;
fLanguage
English
Publisher
ieee
Conference_Titel
Ada Applications and Environments, 1988., Third International IEEE Conference on
Conference_Location
Manchester, NH
Print_ISBN
0-8186-0808-0
Type
conf
DOI
10.1109/ADA.1988.4780
Filename
4780
Link To Document