In the context of formal verification, certifying proofs are evidences of the correctness of a model in a deduction system produced automatically as outcome of the verification. They are quite appealing for high-assurance systems because they can be verified independently by proof checkers, which are usually simpler to certify than the proof-generating tools. Model checking is one of the most prominent approaches to formal verification of temporal properties and is based on an algorithmic search of the system state space. Although modern algorithms integrate deductive methods, the generation of proofs is typically restricted to invariant properties only. Moreover, it assumes that the verification produces an inductive invariant of the original system, while model checkers usually involve a variety of complex pre-processing simplifications. In this paper we show how, exploiting the k-liveness algorithm, to extend proof generation capabilities for invariant checking to cover full linear-time temporal logic (LTL) properties, in a simple and efficient manner, with essentially no overhead for the model checker. Besides the basic k-liveness algorithm, we integrate in the proof generation a variety of widely used pre-processing techniques such as temporal decomposition, model simplification via computation of equivalences with ternary simulation, and the use of stabilizing constraints. These techniques are essential in many cases to prove that a property holds, both for invariant and for LTL model checking, and thus need to be considered within the proof. We implemented the proof generation techniques on top of IC3 engines, and show the feasibility of the approach on a variety of benchmarks taken from the literature and from the Hardware Model Checking Competition. Our results confirm that proof generation results in negligible overhead for the model checker.

Certifying proofs for {SAT}-based model checking / Alberto, Griggio; Roveri, Marco; Stefano, Tonetta; Griggio, Alberto. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - 2021/57:(2021), pp. 178-210. [10.1007/s10703-021-00369-1]

Certifying proofs for {SAT}-based model checking

Marco Roveri;Griggio, Alberto
2021-01-01

Abstract

In the context of formal verification, certifying proofs are evidences of the correctness of a model in a deduction system produced automatically as outcome of the verification. They are quite appealing for high-assurance systems because they can be verified independently by proof checkers, which are usually simpler to certify than the proof-generating tools. Model checking is one of the most prominent approaches to formal verification of temporal properties and is based on an algorithmic search of the system state space. Although modern algorithms integrate deductive methods, the generation of proofs is typically restricted to invariant properties only. Moreover, it assumes that the verification produces an inductive invariant of the original system, while model checkers usually involve a variety of complex pre-processing simplifications. In this paper we show how, exploiting the k-liveness algorithm, to extend proof generation capabilities for invariant checking to cover full linear-time temporal logic (LTL) properties, in a simple and efficient manner, with essentially no overhead for the model checker. Besides the basic k-liveness algorithm, we integrate in the proof generation a variety of widely used pre-processing techniques such as temporal decomposition, model simplification via computation of equivalences with ternary simulation, and the use of stabilizing constraints. These techniques are essential in many cases to prove that a property holds, both for invariant and for LTL model checking, and thus need to be considered within the proof. We implemented the proof generation techniques on top of IC3 engines, and show the feasibility of the approach on a variety of benchmarks taken from the literature and from the Hardware Model Checking Competition. Our results confirm that proof generation results in negligible overhead for the model checker.
2021
Alberto, Griggio; Roveri, Marco; Stefano, Tonetta; Griggio, Alberto
Certifying proofs for {SAT}-based model checking / Alberto, Griggio; Roveri, Marco; Stefano, Tonetta; Griggio, Alberto. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - 2021/57:(2021), pp. 178-210. [10.1007/s10703-021-00369-1]
File in questo prodotto:
File Dimensione Formato  
Griggio2021_Article_CertifyingProofsForSAT-basedMo.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 838.01 kB
Formato Adobe PDF
838.01 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/311268
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 5
social impact