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.
2018
Formal Methods in Computer-Aided Design, FMCAD 2018
Stati Uniti D'America
IEEE
Griggio, Alberto; Roveri, Marco; Tonetta, Stefano
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].
File in questo prodotto:
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

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