Search Results

Documents authored by Nantes-Sobrinho, Daniele

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.25
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner

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

Abstract
The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, but either the function specifications are not validated with respect to the underlying separation logic of the theory, or there is a large gulf between the theory and the implementation of the tool. We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic execution platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce operations used in the engine to update compositionally the symbolic state, for example when calling function specifications. This consume-produce technique is used by VeriFast, Viper, and Gillian, but has not been previously characterised independently of the tool. As part of our result, we give consume and produce operations inspired by the Gillian implementation that satisfy the properties described by our axiomatic interface. A surprising property is that our engine semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this property to extend the Gillian platform, which previously only supported correctness reasoning, with incorrectness reasoning and automatic true bug-finding using incorrectness bi-abduction. We evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool grounded on a common formal compositional symbolic execution engine to support both correctness and incorrectness reasoning.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 25:1-25:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.25,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{25:1--25:28},
  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.25},
  URN =		{urn:nbn:de:0030-drops-208741},
  doi =		{10.4230/LIPIcs.ECOOP.2024.25},
  annote =	{Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.26
Matching Plans for Frame Inference in Compositional Reasoning

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner

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

Abstract
The use of function specifications to reason about function calls and the manipulation of user-defined predicates are two essential ingredients of modern compositional verification tools based on separation logic. To execute these operations successfully, these tools must be able to solve the frame inference problem, that is, to understand which parts of the state are relevant for the operation at hand. We introduce matching plans, a concept that is used in the Gillian verification platform to automate frame inference efficiently. We extract matching plans and their automation machinery from the Gillian implementation and present them in a tool-agnostic way, making the Gillian approach available to the broader verification community as a verification-tool design pattern.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner. Matching Plans for Frame Inference in Compositional Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.26,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Matching Plans for Frame Inference in Compositional Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{26:1--26:20},
  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.26},
  URN =		{urn:nbn:de:0030-drops-208751},
  doi =		{10.4230/LIPIcs.ECOOP.2024.26},
  annote =	{Keywords: Compositional reasoning, separation logic, frame inference}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.13
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimović, and Philippa Gardner

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
This artifact is a companion to the paper "Compositional Symbolic Execution for Correctness and Incorrectness Reasoning". It contains the source code of the Gillian compositional symbolic execution (CSE) platform, in which we added the incorrectness reasoning capabilities, and the benchmarks used in the evaluation of the paper. It also contains a Haskell demonstrator CSE engine that directly implements the CSE engine inference rules presented in the paper.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{loow_et_al:DARTS.10.2.13,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Karmios, Nat and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)}},
  pages =	{13:1--13:2},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Karmios, Nat and Maksimovi\'{c}, Petar and Gardner, Philippa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.13},
  URN =		{urn:nbn:de:0030-drops-209110},
  doi =		{10.4230/DARTS.10.2.13},
  annote =	{Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2021.11
Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes

Authors: Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract
Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that control resource consumption. Our main contribution is the source language, a new resource λ-calculus with non-collapsing non-determinism and failures, dubbed uλ^{↯}_{⊕}. In uλ^{↯}_{⊕}, resources are split into linear and unrestricted; failures are explicit and arise from this distinction. We define a type system based on intersection types to control resources and fail-prone computation. The target language is 𝗌π, an existing session-typed π-calculus that results from a Curry-Howard correspondence between linear logic and session types. Our typed translation subsumes our prior work; interestingly, it treats unrestricted resources in uλ^{↯}_{⊕} as client-server session behaviours in 𝗌π.
Cite as

Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{paulus_et_al:LIPIcs.TYPES.2021.11,
  author =	{Paulus, Joseph W. N. and Nantes-Sobrinho, Daniele and P\'{e}rez, Jorge A.},
  title =	{{Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{11:1--11:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.11},
  URN =		{urn:nbn:de:0030-drops-167808},
  doi =		{10.4230/LIPIcs.TYPES.2021.11},
  annote =	{Keywords: Resource \lambda-calculus, intersection types, session types, process calculi}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.7
Nominal Anti-Unification with Atom-Variables

Authors: Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Anti-unification is the task of generalizing a set of expressions in the most specific way. It was extended to the nominal framework by Baumgarter, Kutsia, Levy and Villaret, who defined an algorithm solving the nominal anti-unification problem, which runs in polynomial time. Unfortunately, when an infinite set of atoms are allowed in generalizations, a minimal complete set of solutions in nominal anti-unification does not exist, in general. In this paper, we present a more general approach to nominal anti-unification that uses atom-variables instead of explicit atoms, and two variants of freshness constraints: NL_A-constraints (with atom-variables), and Eqr-constraints based on Equivalence relations on atom-variables. The idea of atom-variables is that different atom-variables may be instantiated with identical or different atoms. Albeit simple, this freedom in the formulation increases its application potential: we provide an algorithm that is finitary for the NL_A-freshness constraints, and for Eqr-freshness constraints it computes a unique least general generalization. There is a price to pay in the general case: checking freshness constraints and other related logical questions will require exponential time. The setting of Baumgartner et al. is improved by the atom-only case, which runs in polynomial time and computes a unique least general generalization.
Cite as

Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho. Nominal Anti-Unification with Atom-Variables. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2022.7,
  author =	{Schmidt-Schau{\ss}, Manfred and Nantes-Sobrinho, Daniele},
  title =	{{Nominal Anti-Unification with Atom-Variables}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{7:1--7:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.7},
  URN =		{urn:nbn:de:0030-drops-162885},
  doi =		{10.4230/LIPIcs.FSCD.2022.7},
  annote =	{Keywords: Generalization, anti-unification, nominal algorithms, higher-order deduction}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.21
Non-Deterministic Functions as Non-Deterministic Processes

Authors: Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We study encodings of the λ-calculus into the π-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider λ^↯_⊕, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider 𝗌π, a π-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of λ^↯_⊕ into 𝗌π and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in λ^↯_⊕ via typed processes in 𝗌π. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.
Cite as

Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Non-Deterministic Functions as Non-Deterministic Processes. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{paulus_et_al:LIPIcs.FSCD.2021.21,
  author =	{Paulus, Joseph W. N. and Nantes-Sobrinho, Daniele and P\'{e}rez, Jorge A.},
  title =	{{Non-Deterministic Functions as Non-Deterministic Processes}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{21:1--21:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.21},
  URN =		{urn:nbn:de:0030-drops-142598},
  doi =		{10.4230/LIPIcs.FSCD.2021.21},
  annote =	{Keywords: Resource calculi, \pi-calculus, intersection types, session types, linear logic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.7
Fixed-Point Constraints for Nominal Equational Unification

Authors: Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new alpha-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts.
Cite as

Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Fixed-Point Constraints for Nominal Equational Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2018.7,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele},
  title =	{{Fixed-Point Constraints for Nominal Equational Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.7},
  URN =		{urn:nbn:de:0030-drops-91777},
  doi =		{10.4230/LIPIcs.FSCD.2018.7},
  annote =	{Keywords: nominal terms, fixed-point equations, nominal unification, equational theories}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.11
Nominal Narrowing

Authors: Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Nominal unification is a generalisation of first-order unification that takes alpha-equivalence into account. In this paper, we study nominal unification in the context of equational theories. We introduce nominal narrowing and design a general nominal E-unification procedure, which is sound and complete for a wide class of equational theories. We give examples of application.
Cite as

Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal Narrowing. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2016.11,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele},
  title =	{{Nominal Narrowing}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.11},
  URN =		{urn:nbn:de:0030-drops-59832},
  doi =		{10.4230/LIPIcs.FSCD.2016.11},
  annote =	{Keywords: Nominal Rewriting, Nominal Unification, Matching, Narrowing, Equational Theories}
}
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