Symbolic execution-based verification of Ada tasking programs

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