|
Title:
|
Compositional safety verification with Max-SMT
|
|
Author:
|
Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
|
|
Other authors:
|
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació |
|
Abstract:
|
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. |
|
Abstract:
|
Peer Reviewed |
|
Subject(s):
|
-Àrees temàtiques de la UPC::Informàtica::Aplicacions de la informàtica::Disseny assistit per ordinador
-Computer-aided design--Software
-Disseny assistit per ordinador -- Tècniques |
|
Rights:
|
|
|
Document type:
|
Article - Published version
Conference Object |
|
Share:
|
|
