Issue No. 01 - January (1990 vol. 16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.44363
<p>The isolation approach to symbolic execution of Ada tasking programs provides a basis for automating partial correctness proofs. The strength of this approach lies in its isolation nature; tasks are symbolically executed and verified independently, and then checked for cooperation where interference can occur. This keeps the verification task computationally feasible and enhances its compositionality. Safety, however, is a more appropriate notion of correctness for concurrent programs than partial correctness. The author shows how the isolation approach to symbolic execution of Ada tasking program supports the verification of general safety properties. Specific safety properties that are considered include mutual exclusion, freedom from deadlock, and absence of communication failure. The techniques are illustrated using a solution to the readers and writers problem.</p>
safety properties verification; Ada tasking programs; isolation approach; symbolic execution; automating partial correctness proofs; concurrent programs; mutual exclusion; deadlock; Ada; multiprocessing programs; program verification.
L.K. Dillon, "Verifying General Safety Properties of Ada Tasking Programs", IEEE Transactions on Software Engineering, vol. 16, no. , pp. 51-63, January 1990, doi:10.1109/32.44363