Search Results

Documents authored by Gurfinkel, Arie

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.43
Inductive Predicate Synthesis Modulo Programs

Authors: Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the-shelf verifiers, but makes communication with the underlying solver more challenging. Essentially, the analysis tools operates at the level of input programs, whereas the solver operates at the level of problem encodings. To bridge this gap, the verifier must pass along proof-rules from the analysis tool to the solver. For example, an analysis tool for concurrent programs built on an inductive program verifier might need to declare Owicki-Gries style proof-rules for the underlying solver. Each such proof-rule further specifies how a program should be verified, meaning that the problem of passing proof-rules is a form of invariant synthesis. Similarly, many program analysis tasks reduce to the synthesis of pure, loop-free Boolean functions (i.e., predicates), relative to a program. From this observation, we propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features to guide analysis. In IPS-MP, unknown predicates appear under assume and assert statements, acting as specifications modulo the program semantics. Existing synthesis solvers are inefficient at IPS-MP as they target more general problems. In this paper, we show that IPS-MP admits an efficient solution in the Boolean case, despite being generally undecidable. Moreover, we show that IPS-MP reduces to the satisfiability of constrained Horn clauses, which is less general than existing synthesis problems, yet expressive enough to encode verification tasks. We provide reductions from challenging verification tasks - such as parameterized model checking - to IPS-MP. We realize these reductions with an efficient IPS-MP-solver based on SeaHorn, and describe a real-world application to smart-contract verification.
Cite as

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 43:1-43:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wesley_et_al:LIPIcs.ECOOP.2024.43,
  author =	{Wesley, Scott and Christakis, Maria and Navas, Jorge A. and Trefler, Richard and W\"{u}stholz, Valentin and Gurfinkel, Arie},
  title =	{{Inductive Predicate Synthesis Modulo Programs}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{43:1--43:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.43},
  URN =		{urn:nbn:de:0030-drops-208926},
  doi =		{10.4230/LIPIcs.ECOOP.2024.43},
  annote =	{Keywords: Software Verification, Invariant Synthesis, Model-Checking}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2024.1
Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk)

Authors: Arie Gurfinkel

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
First Order Logic (FOL) is a powerful formalism that naturally captures many interesting decision and optimization problems. In recent years, there has been a tremendous progress in automated logic reasoning tools, such as Boolean SATisfiability Solvers and Satisfiability Modulo Theory solvers. This enabled the use of logic and logic solvers as a universal solution to many problems in Computer Science, in general, and in Program Analysis, in particular. Most new program analysis techniques formalize the desired analysis task in a fragment of FOL, and delegate the analysis to a SAT or an SMT solver. In this talk, we focus on a fragment of FOL called Constrained Horn Clauses (CHC) and the CHC solver SPACER. CHCs arise in many applications of automated verification. They naturally capture such problems as discovery and verification of inductive invariants; Model Checking of safety properties of finite- and infinite-state systems; safety verification of push-down systems (and their extensions); modular verification of distributed and parameterized systems; type inference, and many others. Using CHC separates the process of developing a proof methodology (also known as generation of Verification Condition (VC)) from the algorithmic details of deciding whether the VC is correct. Such a flexible design simplifies supporting multiple proof methodologies, multiple languages, and multiple verification tasks with a single framework, without sacrificing performance and scalability.
Cite as

Arie Gurfinkel. Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk). In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gurfinkel:LIPIcs.CONCUR.2024.1,
  author =	{Gurfinkel, Arie},
  title =	{{Constrained Horn Clauses for Program Verification and Synthesis}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.1},
  URN =		{urn:nbn:de:0030-drops-207734},
  doi =		{10.4230/LIPIcs.CONCUR.2024.1},
  annote =	{Keywords: Constrained Horn Clauses}
}
Document
DOI: 10.4230/DagRep.13.7.66
Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281)

Authors: Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, and Anna Becchi

Published in: Dagstuhl Reports, Volume 13, Issue 7 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23281 "Theoretical Advances and Emerging Applications in Abstract Interpretation." Abstract Interpretation (AI) is a theory of the approximation of program semantics. Since its introduction in the 70s, it lead to insights into theoretical research in semantics, a rich and robust mathematical framework to discuss about semantic approximation and program analysis, and the design of effective program analysis tools that are now routinely used in this industry. The seminar brought together academic and industrial partners to assess the state of the art in AI as well as discuss its future. It considered its foundational aspects, connections with other formal methods, emergent applications, user needs in program verification, tool design and evaluation, as well as educational aspects and community management. Its goal was to collect new ideas and new perspectives on all these aspects of AI in order to pave the way for new applications.
Cite as

Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, and Anna Becchi. Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281). In Dagstuhl Reports, Volume 13, Issue 7, pp. 66-95, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{gurfinkel_et_al:DagRep.13.7.66,
  author =	{Gurfinkel, Arie and Mastroeni, Isabella and Min\'{e}, Antoine and M\"{u}ller, Peter and Becchi, Anna},
  title =	{{Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281)}},
  pages =	{66--95},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{7},
  editor =	{Gurfinkel, Arie and Mastroeni, Isabella and Min\'{e}, Antoine and M\"{u}ller, Peter and Becchi, Anna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.7.66},
  URN =		{urn:nbn:de:0030-drops-197759},
  doi =		{10.4230/DagRep.13.7.66},
  annote =	{Keywords: abstract domains, abstract interpretation, program semantics, program verification, static program analysis}
}
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