In the context of formal verification, certifying proofs are proofs 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. In this paper, we solve this issue in the context of Lineartime Temporal Logic. By exploiting the k-liveness algorithm, we show how to extend proof generation capabilities for invariant checking to cover full LTL properties, in a simple and efficient manner, with essentially no overhead for the model checker. We implemented the technique on top of an IC3 engine, and show the feasibility of the approach on a variety of benchmarks.
Certifying Proofs for LTL Model Checking / Griggio, Alberto; Roveri, Marco; Tonetta, Stefano. - (2018), pp. 1-9. (Intervento presentato al convegno Formal Methods in Computer-Aided Design (FMCAD '18) tenutosi a Austin, Texas nel 30 Oct - 2 Nov, 2018) [10.23919/FMCAD.2018.8603022].
Certifying Proofs for LTL Model Checking
Alberto Griggio;Marco Roveri;Stefano Tonetta
2018-01-01
Abstract
In the context of formal verification, certifying proofs are proofs 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. In this paper, we solve this issue in the context of Lineartime Temporal Logic. By exploiting the k-liveness algorithm, we show how to extend proof generation capabilities for invariant checking to cover full LTL properties, in a simple and efficient manner, with essentially no overhead for the model checker. We implemented the technique on top of an IC3 engine, and show the feasibility of the approach on a variety of benchmarks.File | Dimensione | Formato | |
---|---|---|---|
paper_44.pdf
accesso aperto
Tipologia:
Post-print referato (Refereed author’s manuscript)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
332.15 kB
Formato
Adobe PDF
|
332.15 kB | Adobe PDF | Visualizza/Apri |
08603022.pdf
Solo gestori archivio
Tipologia:
Versione editoriale (Publisher’s layout)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
361.64 kB
Formato
Adobe PDF
|
361.64 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione