Efficient symbolic execution of value-based data structures for critical systems

Symbolic execution shows promise for increasing the automation of verification tasks in certified safety/security-critical systems, where use of statically allocated value-based data structures is mandated. In fact Spark/Ada, a subset of Ada designed for verification and used for building critical systems, only permits data structures that are statically allocated. This paper describes a novel and efficient graph-based representation for programs making use of value-based data structures and procedure contracts. We show that our graph-based representation offers performance superior to a logic-based representation that is used in many approaches that delegate array reasoning to a decision procedure.