18 Search Results for "Yang, Hongseok"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.16
Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning

Authors: Cormac Flanagan and Stephen N. Freund

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

Abstract
Rely-guarantee (RG) logic uses thread interference specifications (relies and guarantees) to reason about the correctness of multithreaded software. Unfortunately, RG logic requires each function postcondition to be "stabilized" or specialized to the behavior of other threads, making it difficult to write function specifications that are reusable at multiple call sites. This paper presents mover logic, which extends RG logic to address this problem via the notion of atomic functions. Atomic functions behave as if they execute serially without interference from concurrent threads, and so they can be assigned more general and reusable specifications that avoid the stabilization requirement of RG logic. Several practical verifiers (Calvin-R, QED, CIVL, Armada, Anchor, etc.) have demonstrated the modularity benefits of atomic function specifications. However, the complexity of these systems and their correctness proofs makes it challenging to understand and extend these systems. Mover logic formalizes the central ideas of reduction in a declarative program logic that provides a foundation for future work in this area.
Cite as

Cormac Flanagan and Stephen N. Freund. Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 16:1-16:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{flanagan_et_al:LIPIcs.ECOOP.2024.16,
  author =	{Flanagan, Cormac and Freund, Stephen N.},
  title =	{{Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{16:1--16:29},
  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.16},
  URN =		{urn:nbn:de:0030-drops-208654},
  doi =		{10.4230/LIPIcs.ECOOP.2024.16},
  annote =	{Keywords: concurrent program verification, reduction, rely-guarantee reasoning, synchronization}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.24
Qafny: A Quantum-Program Verifier

Authors: Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu

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

Abstract
Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny’s automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover’s algorithm, and Shor’s algorithm.
Cite as

Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A Quantum-Program Verifier. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 24:1-24:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ECOOP.2024.24,
  author =	{Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi},
  title =	{{Qafny: A Quantum-Program Verifier}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{24:1--24:31},
  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.24},
  URN =		{urn:nbn:de:0030-drops-208735},
  doi =		{10.4230/LIPIcs.ECOOP.2024.24},
  annote =	{Keywords: Quantum Computing, Automated Verification, Separation Logic}
}
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
DOI: 10.4230/LIPIcs.ECOOP.2024.33
Compiling with Arrays

Authors: David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini

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

Abstract
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables. The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (A_{i}NF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. A_{i}NF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to A_{i}NF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.
Cite as

David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. Compiling with Arrays. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{richter_et_al:LIPIcs.ECOOP.2024.33,
  author =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  title =	{{Compiling with Arrays}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{33:1--33:24},
  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.33},
  URN =		{urn:nbn:de:0030-drops-208823},
  doi =		{10.4230/LIPIcs.ECOOP.2024.33},
  annote =	{Keywords: array languages, functional programming, domain-specific languages, normalization by evaluation, common subexpression elimination, polarity, positive function type, intrinsic types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.39
Formalizing, Mechanizing, and Verifying Class-Based Refinement Types

Authors: Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao

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

Abstract
Refinement types have been extensively used in class-based languages to specify and verify fine-grained logical specifications. Despite the advances in practical aspects such as applicability and usability, two fundamental issues persist. First, the soundness of existing class-based refinement type systems is inadequately explored, casting doubts on their reliability. Second, the expressiveness of existing systems is limited, restricting the depiction of semantic properties related to object-oriented constructs. This work tackles these issues through a systematic framework. We formalize a declarative class-based refinement type calculus (named RFJ), that is expressive and concise. We rigorously develop the soundness meta-theory of this calculus, followed by its mechanization in Coq. Finally, to ensure the calculus’s verifiability, we propose an algorithmic verification approach based on a fragment of first-order logic (named LFJ), and implement this approach as a type checker.
Cite as

Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 39:1-39:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{sun_et_al:LIPIcs.ECOOP.2024.39,
  author =	{Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan},
  title =	{{Formalizing, Mechanizing, and Verifying Class-Based Refinement Types}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{39:1--39: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.39},
  URN =		{urn:nbn:de:0030-drops-208881},
  doi =		{10.4230/LIPIcs.ECOOP.2024.39},
  annote =	{Keywords: Refinement Types, Program Verification, Object-oriented Programming}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.45
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers

Authors: David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin

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

Abstract
Synthetic Separation Logic (SSL) is a formalism that powers SuSLik, the state-of-the-art approach for the deductive synthesis of provably-correct programs in C-like languages that manipulate heap-based linked data structures. Despite its expressivity, SSL suffers from two shortcomings that hinder its utility. First, its main specification component, inductive predicates, only admits first-order definitions of data structure shapes, which leads to the proliferation of "boiler-plate" predicates for specifying common patterns. Second, SSL requires concrete definitions of data structures to synthesise programs that manipulate them, which results in the need to change a specification for a synthesis task every time changes are introduced into the layout of the involved structures. We propose to significantly lift the level of abstraction used in writing Separation Logic specifications for synthesis - both simplifying the approach and making the specifications more usable and easy to read and follow. We avoid the need to repetitively re-state low-level representation details throughout the specifications - allowing the reuse of different implementations of the same data structure by abstracting away the details of a specific layout used in memory. Our novel high-level front-end language called Pika significantly improves the expressiveness of SuSLik. We implemented a layout-agnostic synthesiser from Pika to SuSLik enabling push-button synthesis of C programs with in-place memory updates, along with the accompanying full proofs that they meet Separation Logic-style specifications, from high-level specifications that resemble ordinary functional programs. Our experiments show that our tool can produce C code that is comparable in its performance characteristics and is sometimes faster than Haskell.
Cite as

David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin. Higher-Order Specifications for Deductive Synthesis of Programs with Pointers. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 45:1-45:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{young_et_al:LIPIcs.ECOOP.2024.45,
  author =	{Young, David and Yang, Ziyi and Sergey, Ilya and Potanin, Alex},
  title =	{{Higher-Order Specifications for Deductive Synthesis of Programs with Pointers}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{45:1--45:26},
  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.45},
  URN =		{urn:nbn:de:0030-drops-208946},
  doi =		{10.4230/LIPIcs.ECOOP.2024.45},
  annote =	{Keywords: Program Synthesis, Separation Logic, Functional Programming}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.13
Completeness of Asynchronous Session Tree Subtyping in Coq

Authors: Burak Ekici and Nobuko Yoshida

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Multiparty session types (MPST) serve as a foundational framework for formally specifying and verifying message passing protocols. Asynchronous subtyping in MPST allows for typing optimised programs preserving type safety and deadlock freedom under asynchronous interactions where the message order is preserved and sending is non-blocking. The optimisation is obtained by message reordering, which allows for sending messages earlier or receiving them later. Sound subtyping algorithms have been extensively studied and implemented as part of various programming languages and tools including C, Rust and C-MPI. However, formalising all such permutations under sequencing, selection, branching and recursion in session types is an intricate task. Additionally, checking asynchronous subtyping has been proven to be undecidable. This paper introduces the first formalisation of asynchronous subtyping in MPST within the Coq proof assistant. We first decompose session types into session trees that do not involve branching and selection, and then establish a coinductive refinement relation over them to govern subtyping. To showcase our formalisation, we prove example subtyping schemas that appear in the literature, all of which cannot be verified, at the same time, by any of the existing decidable sound algorithms. Additionally, we take the (inductive) negation of the refinement relation from a prior work by Ghilezan et al. [Ghilezan et al., 2023] and re-implement it, significantly reducing the number of rules (from eighteen to eight). We establish the completeness of subtyping with respect to its negation in Coq, addressing the issues concerning the negation rules outlined in the previous work [Ghilezan et al., 2023]. In the formalisation, we use the greatest fixed point of the least fixed point technique, facilitated by the paco library, to define coinductive predicates. We employ parametrised coinduction to prove their properties. The formalisation consists of roughly 10K lines of Coq code, accessible at: https://github.com/ekiciburak/sessionTreeST/tree/itp2024.
Cite as

Burak Ekici and Nobuko Yoshida. Completeness of Asynchronous Session Tree Subtyping in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ekici_et_al:LIPIcs.ITP.2024.13,
  author =	{Ekici, Burak and Yoshida, Nobuko},
  title =	{{Completeness of Asynchronous Session Tree Subtyping in Coq}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{13:1--13:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.13},
  URN =		{urn:nbn:de:0030-drops-207418},
  doi =		{10.4230/LIPIcs.ITP.2024.13},
  annote =	{Keywords: asynchronous multiparty session types, session trees, subtyping, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.19
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic

Authors: Marc Hermes and Robbert Krebbers

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Intrusive linked data structures are commonly used in low-level programming languages such as C for efficiency and to enable a form of generic types. Notably, intrusive versions of linked lists and search trees are used in the Linux kernel and the Boost C++ library. These data structures differ from ordinary data structures in the way that nodes contain only the meta data (i.e. pointers to other nodes), but not the data itself. Instead the programmer needs to embed nodes into the data, thereby avoiding pointer indirections, and allowing data to be part of several data structures. In this paper we address the challenge of specifying and verifying intrusive data structures using separation logic. We aim for modular verification, where we first specify and verify the operations on the nodes (without the data) and then use these specifications to verify clients that attach data. We achieve this by employing a representation predicate that separates the data structure’s node structure from the data that is attached to it. We apply our methodology to singly-linked lists - from which we build cyclic and doubly-linked lists - and binary trees - from which we build binary search trees. All verifications are conducted using the Coq proof assistant, making use of the Iris framework for separation logic.
Cite as

Marc Hermes and Robbert Krebbers. Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hermes_et_al:LIPIcs.ITP.2024.19,
  author =	{Hermes, Marc and Krebbers, Robbert},
  title =	{{Modular Verification of Intrusive List and Tree Data Structures in Separation Logic}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.19},
  URN =		{urn:nbn:de:0030-drops-207478},
  doi =		{10.4230/LIPIcs.ITP.2024.19},
  annote =	{Keywords: Separation Logic, Program Verification, Data Structures, Iris, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.21
A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL

Authors: Michikazu Hirata

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
The Lévy-Prokhorov metric is a metric between finite measures on a metric space. The metric was introduced to analyze weak convergence of measures. We formalize the Lévy-Prokhorov metric and prove Prokhorov’s theorem in Isabelle/HOL. Prokhorov’s theorem provides a condition for the relative compactness of sets of finite measures and plays essential roles in proofs of the central limit theorem, Sanov’s theorem in large deviation theory, and the existence of optimal coupling in transportation theory. Our formalization includes important results in mathematics such as the Riesz representation theorem, which is a theorem in functional analysis and used to prove Prokhorov’s theorem. We also apply the Lévy-Prokhorov metric to show that the measurable space of finite measures on a standard Borel space is again a standard Borel space.
Cite as

Michikazu Hirata. A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hirata:LIPIcs.ITP.2024.21,
  author =	{Hirata, Michikazu},
  title =	{{A Formalization of the L\'{e}vy-Prokhorov Metric in Isabelle/HOL}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.21},
  URN =		{urn:nbn:de:0030-drops-207492},
  doi =		{10.4230/LIPIcs.ITP.2024.21},
  annote =	{Keywords: formalization of mathematics, measure theory, metric spaces, topology, L\'{e}vy-Prokhorov metric, Prokhorov’s theorem, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.23
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras

Authors: Vincent Jackson, Toby Murray, and Christine Rizkallah

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
This paper describes GenRGSep, an Isabelle/HOL library for the development of RGSep logics using a general algebraic state model. In particular, we develop an algebraic state models based on resource algebras that assume neither the presence of unit resources or the cancellativity law. If a new resource model is required, its components need only be proven an instance of a permission algebra, and then they can be composed together using tuples and functions. The proof of soundness is performed by Vafeiadis' operational soundness method. This method was originally formulated with respect to a concrete heap model. This paper adapts it to account for the absence of both units as well as the cancellativity law.
Cite as

Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23,
  author =	{Jackson, Vincent and Murray, Toby and Rizkallah, Christine},
  title =	{{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23},
  URN =		{urn:nbn:de:0030-drops-207510},
  doi =		{10.4230/LIPIcs.ITP.2024.23},
  annote =	{Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.30
Around Classical and Intuitionistic Linear Processes

Authors: Juan C. Jaramillo, Dan Frumin, and Jorge A. Pérez

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

Abstract
Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classical versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent, we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey. Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.
Cite as

Juan C. Jaramillo, Dan Frumin, and Jorge A. Pérez. Around Classical and Intuitionistic Linear Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jaramillo_et_al:LIPIcs.CONCUR.2024.30,
  author =	{Jaramillo, Juan C. and Frumin, Dan and P\'{e}rez, Jorge A.},
  title =	{{Around Classical and Intuitionistic Linear Processes}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{30:1--30:19},
  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.30},
  URN =		{urn:nbn:de:0030-drops-208026},
  doi =		{10.4230/LIPIcs.CONCUR.2024.30},
  annote =	{Keywords: Process calculi, session types, linear logic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.18
Representation of Peano Arithmetic in Separation Logic

Authors: Sohei Ito and Makoto Tatsuta

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.
Cite as

Sohei Ito and Makoto Tatsuta. Representation of Peano Arithmetic in Separation Logic. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ito_et_al:LIPIcs.FSCD.2024.18,
  author =	{Ito, Sohei and Tatsuta, Makoto},
  title =	{{Representation of Peano Arithmetic in Separation Logic}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.18},
  URN =		{urn:nbn:de:0030-drops-203476},
  doi =		{10.4230/LIPIcs.FSCD.2024.18},
  annote =	{Keywords: First order logic, Separation logic, Peano arithmetic, Presburger arithmetic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.20
On Iteration in Discrete Probabilistic Programming

Authors: Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva, and Fabio Zanasi

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Discrete probabilistic programming languages provide an expressive tool for representing and reasoning about probabilistic models. These languages typically define the semantics of a program through its posterior distribution, obtained through exact inference techniques. While the semantics of standard programming constructs in this context is well understood, there is a gap in extending these languages with tools to reason about the asymptotic behaviour of programs. In this paper, we introduce unbounded iteration in the context of a discrete probabilistic programming language, give it a semantics, and show how to compute it exactly. This allows us to express the stationary distribution of a probabilistic function while preserving the efficiency of exact inference techniques. We discuss the advantages and limitations of our approach, showcasing their practical utility by considering examples where bounded iteration poses a challenge due to the inherent difficulty of assessing the proximity of a distribution to its stationary point.
Cite as

Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva, and Fabio Zanasi. On Iteration in Discrete Probabilistic Programming. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{torresruiz_et_al:LIPIcs.FSCD.2024.20,
  author =	{Torres-Ruiz, Mateo and Piedeleu, Robin and Silva, Alexandra and Zanasi, Fabio},
  title =	{{On Iteration in Discrete Probabilistic Programming}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{20:1--20:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.20},
  URN =		{urn:nbn:de:0030-drops-203490},
  doi =		{10.4230/LIPIcs.FSCD.2024.20},
  annote =	{Keywords: Probabilistic programming, Programming languages semantics, Unbounded iteration}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2019.4
Some Semantic Issues in Probabilistic Programming Languages (Invited Talk)

Authors: Hongseok Yang

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
This is a slightly extended abstract of my talk at FSCD'19 about probabilistic programming and a few semantic issues on it. The main purpose of this abstract is to provide keywords and references on the work mentioned in my talk, and help interested audience to do follow-up study.
Cite as

Hongseok Yang. Some Semantic Issues in Probabilistic Programming Languages (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{yang:LIPIcs.FSCD.2019.4,
  author =	{Yang, Hongseok},
  title =	{{Some Semantic Issues in Probabilistic Programming Languages}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{4:1--4:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.4},
  URN =		{urn:nbn:de:0030-drops-105118},
  doi =		{10.4230/LIPIcs.FSCD.2019.4},
  annote =	{Keywords: Probabilistic Programming, Denotational Semantics, Non-differentiable Models, Bayesian Nonparametrics, Exchangeability}
}
  • Refine by Author
  • 4 Yang, Hongseok
  • 2 Ayoun, Sacha-Élie
  • 2 Gardner, Philippa
  • 2 Lööw, Andreas
  • 2 Maksimović, Petar
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Separation logic
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Program verification
  • 2 Software and its engineering → Formal software verification
  • 2 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 3 Probabilistic programming
  • 3 Separation Logic
  • 3 separation logic
  • 2 Coq
  • 2 Exchangeability
  • Show More...

  • Refine by Type
  • 18 document

  • Refine by Publication Year
  • 14 2024
  • 2 2017
  • 1 2018
  • 1 2019

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