Using symbolic execution for verification of Ada tasking programs

Publisher Website
Google Scholar
Abstract
A method is presented for using symbolic execution to generate the verification conditions required for proving correctness of programs written in a tasking subset of Ada. The symbolic execution rules are derived from proof systems that allow tasks to be verified independently in local proofs, which are then checked for cooperation. The isolation nature of this approach to symbolic execution of concurrent programs makes it better suited to formal verification than the more traditional interleaving approach, which suffers from combinatorial problems. The criteria for correct operation of a concurrent program include partial correctness, as well as more general safety properties, such as mutual exclusion and freedom from deadlock.

This publication has 13 references indexed in Scilit: