Compositional safety verification with Max-SMT
Document typeConference report
Rights accessOpen Access
We present an automated compositional program verification technique for safety properties based on conditional inductive invariants. For a given program part (e.g., a single loop) and a postcondition, we show how to, using a Max-SMT solver, an inductive invariant together with a precondition can be synthesized so that the precondition ensures the validity of the invariant and that the invariant implies the postcondition. From this, we build a bottom-up program verification framework that propagates preconditions of small program parts as postconditions for preceding program parts. The method recovers from failures to prove the validity of a precondition, using the obtained intermediate results to restrict the search space for further proof attempts. As only small program parts need to be handled at a time, our method is scalable and distributable. The derived conditions can be viewed as implicit contracts between different parts of the program, and thus enable an incremental program analysis.
CitationBrockschmidt, M., Larraz, D., Oliveras, A., Rodriguez, E., Rubio, A. Compositional safety verification with Max-SMT. A: International Conference on Formal Methods in Computer-Aided Design. "FMCAD 2015 : 15th International Conference on Formal Methods in Computer-Aided Design: Austin, Texas, USA: September 27-30, 2015: proceedings book". Austin, Texas: 2015, p. 33-40.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder