Efficient Certified Resolution Proof Checking

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

100 Downloads (Pure)

Resumé

We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders of magnitude. We then formalize the theory underlying propositional proof checking in Coq, and extract a correct-by-construction proof checker for our format from the formalization. An empirical evaluation using 280 unsatisfiable instances from the 2015 and 2016 SAT competitions shows that this certified checker usually performs comparably to a state-of-the-art non-certified proof checker. Using this format, we formally verify the recent 200 TB proof of the Boolean Pythagorean Triples conjecture.
OriginalsprogEngelsk
TitelTools and Algorithms for the Construction and Analysis of Systems : Proceedings of the 3rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017
RedaktørerAxel Legay, Tiziana Margaria
Vol/bindPart I
ForlagSpringer
Publikationsdato2017
Sider118-135
ISBN (Trykt)978-3-662-54576-8
ISBN (Elektronisk)978-3-662-54577-5
DOI
StatusUdgivet - 2017
Begivenhed23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Uppsala, Sverige
Varighed: 22. apr. 201729. apr. 2017
Konferencens nummer: 23

Konference

Konference23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Nummer23
LandSverige
ByUppsala
Periode22/04/201729/04/2017
NavnLecture Notes in Computer Science
Vol/bind10205
ISSN0302-9743

Fingeraftryk

Processing

Citer dette

Cruz-Filipe, L., Marques-Silva, J., & Schneider-Kamp, P. (2017). Efficient Certified Resolution Proof Checking. I A. Legay, & T. Margaria (red.), Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 3rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017 (Bind Part I, s. 118-135). Springer. Lecture Notes in Computer Science, Bind. 10205 https://doi.org/10.1007/978-3-662-54577-5_7
Cruz-Filipe, Luís ; Marques-Silva, Joao ; Schneider-Kamp, Peter. / Efficient Certified Resolution Proof Checking. Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 3rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017. red. / Axel Legay ; Tiziana Margaria. Bind Part I Springer, 2017. s. 118-135 (Lecture Notes in Computer Science, Bind 10205).
@inproceedings{80cad6ac1740458eab0c0012ad3a6db5,
title = "Efficient Certified Resolution Proof Checking",
abstract = "We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders of magnitude. We then formalize the theory underlying propositional proof checking in Coq, and extract a correct-by-construction proof checker for our format from the formalization. An empirical evaluation using 280 unsatisfiable instances from the 2015 and 2016 SAT competitions shows that this certified checker usually performs comparably to a state-of-the-art non-certified proof checker. Using this format, we formally verify the recent 200 TB proof of the Boolean Pythagorean Triples conjecture.",
author = "Lu{\'i}s Cruz-Filipe and Joao Marques-Silva and Peter Schneider-Kamp",
year = "2017",
doi = "10.1007/978-3-662-54577-5_7",
language = "English",
isbn = "978-3-662-54576-8",
volume = "Part I",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "118--135",
editor = "Axel Legay and Tiziana Margaria",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "Germany",

}

Cruz-Filipe, L, Marques-Silva, J & Schneider-Kamp, P 2017, Efficient Certified Resolution Proof Checking. i A Legay & T Margaria (red), Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 3rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017. bind Part I, Springer, Lecture Notes in Computer Science, bind 10205, s. 118-135, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sverige, 22/04/2017. https://doi.org/10.1007/978-3-662-54577-5_7

Efficient Certified Resolution Proof Checking. / Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter.

Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 3rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017. red. / Axel Legay; Tiziana Margaria. Bind Part I Springer, 2017. s. 118-135 (Lecture Notes in Computer Science, Bind 10205).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - Efficient Certified Resolution Proof Checking

AU - Cruz-Filipe, Luís

AU - Marques-Silva, Joao

AU - Schneider-Kamp, Peter

PY - 2017

Y1 - 2017

N2 - We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders of magnitude. We then formalize the theory underlying propositional proof checking in Coq, and extract a correct-by-construction proof checker for our format from the formalization. An empirical evaluation using 280 unsatisfiable instances from the 2015 and 2016 SAT competitions shows that this certified checker usually performs comparably to a state-of-the-art non-certified proof checker. Using this format, we formally verify the recent 200 TB proof of the Boolean Pythagorean Triples conjecture.

AB - We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders of magnitude. We then formalize the theory underlying propositional proof checking in Coq, and extract a correct-by-construction proof checker for our format from the formalization. An empirical evaluation using 280 unsatisfiable instances from the 2015 and 2016 SAT competitions shows that this certified checker usually performs comparably to a state-of-the-art non-certified proof checker. Using this format, we formally verify the recent 200 TB proof of the Boolean Pythagorean Triples conjecture.

U2 - 10.1007/978-3-662-54577-5_7

DO - 10.1007/978-3-662-54577-5_7

M3 - Article in proceedings

SN - 978-3-662-54576-8

VL - Part I

T3 - Lecture Notes in Computer Science

SP - 118

EP - 135

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Legay, Axel

A2 - Margaria, Tiziana

PB - Springer

ER -

Cruz-Filipe L, Marques-Silva J, Schneider-Kamp P. Efficient Certified Resolution Proof Checking. I Legay A, Margaria T, red., Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 3rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017. Bind Part I. Springer. 2017. s. 118-135. (Lecture Notes in Computer Science, Bind 10205). https://doi.org/10.1007/978-3-662-54577-5_7