Abstract
Model checking is used widely as a formal verification technique for safety-critical systems. Certifying the correctness of model checking results helps increasing confidence in the verification procedure. This can be achieved by additional book-keeping inside existing model checkers. Based on this, we extended an existing BDD-based model checker as well as an IC3-based incremental inductive model checker, to generate certificates during the model checking procedure. We also introduce a proof checker which provides a standardised way to validate certificates generated from model checkers in conjunction with a SAT solver. The main goal is to establish a certification process for the hardware model checking competition.
| Original language | English |
|---|---|
| Title of host publication | Formal Methods and Software Engineering : 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5–9, 2019, Proceedings |
| Editors | Yamine Ait-Ameur, Shengchao Qin |
| Number of pages | 5 |
| Place of Publication | Cham |
| Publisher | Springer International Publishing AG |
| Publication date | 28 Oct 2019 |
| Pages | 498-502 |
| ISBN (Print) | 978-3-030-32408-7 |
| ISBN (Electronic) | 978-3-030-32409-4 |
| DOIs | |
| Publication status | Published - 28 Oct 2019 |
| MoE publication type | A4 Article in conference proceedings |
| Event | International Conference on Formal Engineering Methods - Shenzen, China Duration: 5 Nov 2019 → 9 Nov 2019 Conference number: 21 http://csse.szu.edu.cn/icfem2019/ |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 11852 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Fields of Science
- 113 Computer and information sciences