Search Results

Documents authored by Tinelli, Cesare

Document
Invited Talk
DOI: 10.4230/LIPIcs.SAT.2024.2
Scalable Proof Production and Checking in SMT (Invited Talk)

Authors: Cesare Tinelli

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Solvers for Satisfiability Modulo Theories (SMT) have become crucial components in safety- or mission-critical formal methods applications, in particular model checking, verification, and security analysis. Since state-of-the-art SMT solvers are large and complex systems, they are prohibitively difficult to prove correct. Hence, proof production is essential as a way to demonstrate instead the correctness of their responses, making those responses amenable to independent verification. Historically, the main challenges for proof production in SMT have been solver performance and proof coverage, often leading to the disabling of many sophisticated solving techniques when running in proof-production mode, or to coarse-grained, and harder to check, proofs. The first part of this talk presents a flexible proof-production architecture designed to handle the complexity of versatile, industrial-strength SMT solvers, and discusses how it has been leveraged to produce detailed proofs, even for sophisticated reasoning components. The architecture, implemented in the state-of-the-art SMT solver cvc5, allows proofs to be produced modularly, as needed, and with various safeguards for correctness. The architecture supports the generation of textual proof certificates in different formats, for offline proof checking by external tools, as well as a rich API, which is useful for online integration of the SMT solver into other reasoning tools such as, for instance, skeptical proof assistants. Extensive experimental evaluations with both SMT-LIB benchmarks and benchmarks provided by industrial partners have shown that the new architecture results in greater proof coverage than previous approaches, imposes a small runtime overhead, and supports fine-grained proofs in the great majority of cases. The second part of the talk gives an overview of a new generic language for expressing SMT proof certificates that builds on almost two decades of work and experience in proof generation and checking in SMT and combines the benefits of several previous efforts on the topic. While developed to express cvc5’s proof certificates, the language is meant to be useful to other SMT solvers as well. It is in fact a logical framework, based on the syntax and semantics of the upcoming Version 3 of the SMT-LIB standard, that can be customized, as in the case of cvc5, with the specific proof system used by the solver through the definition of new symbols, binders and proof rules. In addition, it features an intuitive syntax for representing natural-deduction-style proofs and the ability to integrate other proof formats (such as, for instance, those currently used by SAT solvers) via the use of oracles. The talk discusses an initial evaluation of the proof language, obtained with a companion checker for it and an instantiation to cvc5’s proof system. The evaluation shows the viability of high-performance, fine-grained proof production and checking for SMT. The talk concludes with a brief overview of future work and new potential applications enabled by scalable proof certificate production and checking.
Cite as

Cesare Tinelli. Scalable Proof Production and Checking in SMT (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{tinelli:LIPIcs.SAT.2024.2,
  author =	{Tinelli, Cesare},
  title =	{{Scalable Proof Production and Checking in SMT}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.2},
  URN =		{urn:nbn:de:0030-drops-205241},
  doi =		{10.4230/LIPIcs.SAT.2024.2},
  annote =	{Keywords: Satisfiability Modulo Theories, Proof generation and certification}
}
Document
DOI: 10.4230/DagRep.9.9.23
Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)

Authors: Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli

Published in: Dagstuhl Reports, Volume 9, Issue 9 (2020)

Abstract
Research in automated deduction is traditionally focused on the problem of determining the satisfiability of formulas or, more generally, on solving logical problems with yes/no answers. Thanks to recent advances that have dramatically increased the power of automated deduction tools, there is now a growing interest in extending deduction techniques to attack logical problems with more complex answers. These include both problems with a long history, such as quantifier elimination, which are now being revisited in light of the new methods, as well as newer problems such as minimal unsatisfiable cores computation, model counting for propositional or first-order formulas, Boolean or SMT constraint optimization, generation of interpolants, abductive reasoning, and syntax-guided synthesis. Such problems arise in a variety of applications including the analysis of probabilistic systems (where properties like safety or liveness can be established only probabilistically), network verification (with relies on model counting), the computation of tight complexity bounds for programs, program synthesis, model checking (where interpolation or abductive reasoning can be used to achieve scale), and ontology-based information processing. The seminar brought together researchers and practitioners from many of the often disjoint sub-communities interested in the problems above. The unifying theme of the seminar was how to harness and extend the power of automated deduction methods to solve problems with more complex answers than binary ones.
Cite as

Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli. Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). In Dagstuhl Reports, Volume 9, Issue 9, pp. 23-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{fuhs_et_al:DagRep.9.9.23,
  author =	{Fuhs, Carsten and R\"{u}mmer, Philipp and Schmidt, Renate and Tinelli, Cesare},
  title =	{{Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)}},
  pages =	{23--44},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{9},
  editor =	{Fuhs, Carsten and R\"{u}mmer, Philipp and Schmidt, Renate and Tinelli, Cesare},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.9.23},
  URN =		{urn:nbn:de:0030-drops-118432},
  doi =		{10.4230/DagRep.9.9.23},
  annote =	{Keywords: abduction, automated deduction, interpolation, quantifier elimination, synthesis}
}
Document
DOI: 10.4230/DagRep.7.9.26
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)

Authors: Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli

Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17371 "Deduction Beyond First-Order Logic." Much research in the past two decades was dedicated to automating first-order logic with equality. However, applications often need reasoning beyond this logic. This includes genuinely higher-order reasoning, reasoning in theories that are not finitely axiomatisable in first-order logic (such as those including transitive closure operators or standard arithmetic on integers or reals), or reasoning by mathematical induction. Other practical problems need a mixture of first-order proof search and some more advanced reasoning (for instance, about higher-order formulas), or simply higher-level reasoning steps. The aim of the seminar was to bring together first-order automated reasoning experts and researchers working on deduction methods and tools that go beyond first-order logic. The seminar was dedicated to the exchange of ideas to facilitate the transition from first-order to more expressive settings.
Cite as

Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli. Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). In Dagstuhl Reports, Volume 7, Issue 9, pp. 26-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{blanchette_et_al:DagRep.7.9.26,
  author =	{Blanchette, Jasmin Christian and Fuhs, Carsten and Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
  title =	{{Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)}},
  pages =	{26--46},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Blanchette, Jasmin Christian and Fuhs, Carsten and Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.9.26},
  URN =		{urn:nbn:de:0030-drops-85872},
  doi =		{10.4230/DagRep.7.9.26},
  annote =	{Keywords: Automated Deduction, Program Verification, Certification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact