Search Results

Documents authored by Christakis, Maria

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
DOI: 10.4230/DagRep.13.3.92
Software Bug Detection: Challenges and Synergies (Dagstuhl Seminar 23131)

Authors: Marcel Böhme, Maria Christakis, Rohan Padhye, Kostya Serebryany, Andreas Zeller, and Hasan Ferit Eniser

Published in: Dagstuhl Reports, Volume 13, Issue 3 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23131 "Software Bug Detection: Challenges and Synergies". This seminar brought together researchers from academia and industry working on various aspects of software bug detection, with two broad goals: identifying challenges in practical deployment of bug-finding tools and discovering new synergies among bug-finding techniques and research methods. The seminar focused discussion on bug-finding tools and their relevance and adoption in industry.
Cite as

Marcel Böhme, Maria Christakis, Rohan Padhye, Kostya Serebryany, Andreas Zeller, and Hasan Ferit Eniser. Software Bug Detection: Challenges and Synergies (Dagstuhl Seminar 23131). In Dagstuhl Reports, Volume 13, Issue 3, pp. 92-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{bohme_et_al:DagRep.13.3.92,
  author =	{B\"{o}hme, Marcel and Christakis, Maria and Padhye, Rohan and Serebryany, Kostya and Zeller, Andreas and Eniser, Hasan Ferit},
  title =	{{Software Bug Detection: Challenges and Synergies (Dagstuhl Seminar 23131)}},
  pages =	{92--105},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{13},
  number =	{3},
  editor =	{B\"{o}hme, Marcel and Christakis, Maria and Padhye, Rohan and Serebryany, Kostya and Zeller, Andreas and Eniser, Hasan Ferit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.3.92},
  URN =		{urn:nbn:de:0030-drops-192308},
  doi =		{10.4230/DagRep.13.3.92},
  annote =	{Keywords: Bug Finding, Coverage, ML4SE, Oracles, Software Testing, Software Verification}
}
Document
DOI: 10.4230/DagRep.11.9.80
Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)

Authors: Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu

Published in: Dagstuhl Reports, Volume 11, Issue 9 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21431 "Rigorous Methods for Smart Contracts". Blockchain technologies have emerged as an exciting field for both researchers and practitioners focusing on formal guarantees for software. It is arguably a "once in a lifetime" opportunity for rigorous methods to be integrated in audit processes for parties deploying smart contracts, whether for fund raising, securities trading, or supply-chain management. Smart contracts are programs managing cryptocurrency accounts on a blockchain. Research in the area of smart contracts includes a fascinating combination of formal methods, programming-language semantics, and cryptography. First, there is vibrant development of verification and program-analysis techniques that check the correctness of smart-contract code. Second, there are emerging designs of programming languages and methodologies for writing smart contracts such that they are more robust by construction or more amenable to analysis and verification. Programming-language abstraction layers expose low-level cryptographic primitives enabling developers to design high-level cryptographic protocols. Automated-reasoning mechanisms present a common underlying enabler; and the specific needs of the smart-contract world offer new challenges. This workshop brought together stakeholders in the aforementioned areas related to advancing reliable smart-contract technologies.
Cite as

Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu. Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). In Dagstuhl Reports, Volume 11, Issue 9, pp. 80-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{bjrner_et_al:DagRep.11.9.80,
  author =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  title =	{{Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)}},
  pages =	{80--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{9},
  editor =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.9.80},
  URN =		{urn:nbn:de:0030-drops-159198},
  doi =		{10.4230/DagRep.11.9.80},
  annote =	{Keywords: automated reasoning, cryptographic protocols, program verification, programming languages, smart contracts}
}
Document
DOI: 10.4230/DagRep.11.10.20
Ensuring the Reliability and Robustness of Database Management Systems (Dagstuhl Seminar 21442)

Authors: Alexander Böhm, Maria Christakis, Eric Lo, and Manuel Rigger

Published in: Dagstuhl Reports, Volume 11, Issue 10 (2022)

Abstract
The goal of this seminar was to bring together researchers and practitioners from various domains such as of databases, automatic testing, and formal methods to build a common ground and to explore possibilities for systematically improving the state of the art in database management system engineering. The outcome of the seminar was a joint understanding of the specific intricacies of building stateful system software, as well as the identification of several areas of future work. In particular, we believe that database system engineering can both be significantly improved by adopting additional verification techniques and testing tools, and can provide important feedback and additional challenges (e.g. related to state management) to neighboring domains.
Cite as

Alexander Böhm, Maria Christakis, Eric Lo, and Manuel Rigger. Ensuring the Reliability and Robustness of Database Management Systems (Dagstuhl Seminar 21442). In Dagstuhl Reports, Volume 11, Issue 10, pp. 20-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{bohm_et_al:DagRep.11.10.20,
  author =	{B\"{o}hm, Alexander and Christakis, Maria and Lo, Eric and Rigger, Manuel},
  title =	{{Ensuring the Reliability and Robustness of Database Management Systems (Dagstuhl Seminar 21442)}},
  pages =	{20--35},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{10},
  editor =	{B\"{o}hm, Alexander and Christakis, Maria and Lo, Eric and Rigger, Manuel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.10.20},
  URN =		{urn:nbn:de:0030-drops-159269},
  doi =		{10.4230/DagRep.11.10.20},
  annote =	{Keywords: Databases, Reliability, Robustness, Testing, Dagstuhl Seminar}
}
Document
Front Matter
DOI: 10.4230/DARTS.5.2.0
Front Matter - ECOOP 2019 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee

Authors: Maria Christakis and Manuel Rigger

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Front Matter - ECOOP 2019 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Cite as

Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 0:i-0:xi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{christakis_et_al:DARTS.5.2.0,
  author =	{Christakis, Maria and Rigger, Manuel},
  title =	{{Front Matter - ECOOP 2019 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}},
  pages =	{0:i--0:xi},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{Christakis, Maria and Rigger, Manuel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.0},
  URN =		{urn:nbn:de:0030-drops-107779},
  doi =		{10.4230/DARTS.5.2.0},
  annote =	{Keywords: Front Matter - ECOOP 2019 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}
}
Document
DOI: 10.4230/DARTS.4.3.0
Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee

Authors: Maria Christakis, Philipp Haller, Marianna Rapoport, and Marianna Rapoport

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Cite as

Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{christakis_et_al:DARTS.4.3.0,
  author =	{Christakis, Maria and Haller, Philipp and Rapoport, Marianna and Rapoport, Marianna},
  title =	{{Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}},
  pages =	{0:i--0:xii},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Christakis, Maria and Haller, Philipp and Rapoport, Marianna and Rapoport, Marianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.0},
  URN =		{urn:nbn:de:0030-drops-92327},
  doi =		{10.4230/DARTS.4.3.0},
  annote =	{Keywords: Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}
}
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 Imprint Privacy Contact