25 Search Results for "Gardner, Philippa"


Document
Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding

Authors: Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)


Abstract
Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised. We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.

Cite as

Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 19:1-19:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{maksimovic_et_al:LIPIcs.ECOOP.2023.19,
  author =	{Maksimovi\'{c}, Petar and Cronj\"{a}ger, Caroline and L\"{o}\"{o}w, Andreas and Sutherland, Julian and Gardner, Philippa},
  title =	{{Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{19:1--19:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim 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.2023.19},
  URN =		{urn:nbn:de:0030-drops-182123},
  doi =		{10.4230/LIPIcs.ECOOP.2023.19},
  annote =	{Keywords: Separation logic, program correctness, program incorrectness, abstraction}
}
Document
Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure

Authors: Gal Amram, Avi Hayoun, Lior Mizrahi, and Gera Weiss

Published in: LIPIcs, Volume 246, 36th International Symposium on Distributed Computing (DISC 2022)


Abstract
We analyze correctness of implementations of the snapshot data structure in terms of linearizability. We show that such implementations can be verified in polynomial time. Additionally, we identify a set of representative executions for testing and show that the correctness of each of these executions can be validated in linear time. These results present a significant speedup considering that verifying linearizability of implementations of concurrent data structures, in general, is EXPSPACE-complete in the number of program-states, and testing linearizability is NP-complete in the length of the tested execution. The crux of our approach is identifying a class of executions, which we call simple, such that a snapshot implementation is linearizable if and only if all of its simple executions are linearizable. We then divide all possible non-linearizable simple executions into three categories and construct a small automaton that recognizes each category. We describe two implementations (one for verification and one for testing) of an automata-based approach that we develop based on this result and an evaluation that demonstrates significant improvements over existing tools. For verification, we show that restricting a state-of-the-art tool to analyzing only simple executions saves resources and allows the analysis of more complex cases. Specifically, restricting attention to simple executions finds bugs in 27 instances, whereas, without this restriction, we were only able to find 14 of the 30 bugs in the instances we examined. We also show that our technique accelerates testing performance significantly. Specifically, our implementation solves the complete set of 900 problems we generated, whereas the state-of-the-art linearizability testing tool solves only 554 problems.

Cite as

Gal Amram, Avi Hayoun, Lior Mizrahi, and Gera Weiss. Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{amram_et_al:LIPIcs.DISC.2022.5,
  author =	{Amram, Gal and Hayoun, Avi and Mizrahi, Lior and Weiss, Gera},
  title =	{{Polynomial-Time Verification and Testing of Implementations of the Snapshot Data Structure}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2022.5},
  URN =		{urn:nbn:de:0030-drops-171964},
  doi =		{10.4230/LIPIcs.DISC.2022.5},
  annote =	{Keywords: Snapshot, Linearizability, Verification, Formal Methods}
}
Document
Invited Talk
Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk)

Authors: Philippa Gardner

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)


Abstract
Scalable verification for concurrent programs with shared memory is a long-standing, difficult problem. In 2004, O'Hearn and Brookes introduced concurrent separation logic to provide compositional reasoning about coarse-grained concurrent programs with synchronisation primitives (Gödel prize, 2016). In 2010, I introduced logical abstraction (the fiction of separation) to CSL, developing the CAP logic for reasoning about fine-grained concurrent programs in general and fine-grained lock algorithms in particular. In one logic, it was possible to provide two-sided specifications of concurrent operations, with formally verified implementations and clients. In 2014, I introduced logical atomicity (the fiction of atomicity) to concurrent separation logics, developing the TaDA logic to capture when individual operations behave atomically. Unlike CAP, where synchronisation primitives leak into the specifications, with TaDA the specifications are "just right" in that they provide more general atomic functions specifications to capture, for example, the full behaviour of lock operations. In 2021, I introduced environment liveness conditions to concurrent separation logics, developing the TaDA Live logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. The fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. In this talk, I will explain this on-going journey in the wonderful world of concurrent separation logics. I will also explain why I have a bright green office chair in the corner of my office, patterned in gold lamé. Many thanks to my fabulous coauthors on concurrent separation logics: Thomas Dinsdale-Young, Emanuele D'Osualdo, Mike Dodds, Azadeh Farzan, Matthew Parkinson, Pedro da Rocha Pinto, Julian Sutherland, Viktor Vafeiadis and more. Suggested Reading: - Peter O'Hearn: Resources, Concurrency and Local Reasoning, Journal of Theoretical Computer Science, Festschrift for John C Reynolds 70th birthday, 2007. - Thomas Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner: A Perspective on Specifying and Verifying Concurrent Modules, Journal of Logical and Algebraic Methods in Programming, 2018. - Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner and Julian Sutherland: TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), 2021.

Cite as

Philippa Gardner. Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{gardner:LIPIcs.CONCUR.2022.2,
  author =	{Gardner, Philippa},
  title =	{{Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.2},
  URN =		{urn:nbn:de:0030-drops-170659},
  doi =		{10.4230/LIPIcs.CONCUR.2022.2},
  annote =	{Keywords: Concurrent separation logic}
}
Document
Artifact
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact)

Authors: Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
This artifact contains the implementation of JaVerT.Click, a symbolic analysis tool for modern event-driven Web applications. The tool extends JaVerT 2.0, a state-of-the-art symbolic execution tool for JavaScript (JS), with JS reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics which is sufficiently expressive to describe the event models underlying these APIs. Our reference implementations mostly follow the respective standards line-by-line and are all thoroughly tested against the official test suite. We also evaluate JaVerT.Click by performing symbolic analysis on two real-world libraries: cash and p-map, finding three previously unknown bugs.

Cite as

Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@Article{sampaio_et_al:DARTS.6.2.5,
  author =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact)}},
  pages =	{5:1--5:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} 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.6.2.5},
  URN =		{urn:nbn:de:0030-drops-132028},
  doi =		{10.4230/DARTS.6.2.5},
  annote =	{Keywords: Events, DOM, JavaScript, promises, symbolic execution, bug-finding}
}
Document
Data Consistency in Transactional Storage Systems: A Centralised Semantics

Authors: Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. Using our abstract states, we present operational definitions of well-known consistency models in the literature, and prove them to be equivalent to their existing declarative definitions using abstract executions. We explore two applications of our operational framework: 1) verifying that the COPS replicated database and the Clock-SI partitioned database satisfy their consistency models using trace refinement, and 2) proving invariant properties of client programs.

Cite as

Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. Data Consistency in Transactional Storage Systems: A Centralised Semantics. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 21:1-21:31, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{xiong_et_al:LIPIcs.ECOOP.2020.21,
  author =	{Xiong, Shale and Cerone, Andrea and Raad, Azalea and Gardner, Philippa},
  title =	{{Data Consistency in Transactional Storage Systems: A Centralised Semantics}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{21:1--21:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.21},
  URN =		{urn:nbn:de:0030-drops-131782},
  doi =		{10.4230/LIPIcs.ECOOP.2020.21},
  annote =	{Keywords: Operational Semantics, Consistency Models, Transactions, Distributed Key-value Stores}
}
Document
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

Authors: Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
We introduce a trusted infrastructure for the symbolic analysis of modern event-driven Web applications. This infrastructure consists of reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics which is sufficiently expressive to describe the event models underlying these APIs. Our reference implementations are trustworthy in that three follow the appropriate standards line-by-line and all are thoroughly tested against the official test-suites, passing all the applicable tests. Using the Core Event Semantics and the reference implementations, we develop JaVerT.Click, a symbolic execution tool for JavaScript that, for the first time, supports reasoning about JavaScript programs that use multiple event-related APIs. We demonstrate the viability of JaVerT.Click by proving both the presence and absence of bugs in real-world JavaScript code.

Cite as

Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 28:1-28:29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{sampaio_et_al:LIPIcs.ECOOP.2020.28,
  author =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{28:1--28:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.28},
  URN =		{urn:nbn:de:0030-drops-131853},
  doi =		{10.4230/LIPIcs.ECOOP.2020.28},
  annote =	{Keywords: Events, DOM, JavaScript, promises, symbolic execution, bug-finding}
}
Document
K-LLVM: A Relatively Complete Semantics of LLVM IR

Authors: Liyi Li and Elsa L. Gunter

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
LLVM [Lattner and Adve, 2004] is designed for the compile-time, link-time and run-time optimization of programs written in various programming languages. The language supported by LLVM targeted by modern compilers is LLVM IR [llvm.org, 2018]. In this paper we define K-LLVM, a reference semantics for LLVM IR. To the best of our knowledge, K-LLVM is the most complete formal LLVM IR semantics to date, including all LLVM IR instructions, intrinsic functions in the LLVM documentation and Standard-C library functions that are necessary to execute many LLVM IR programs. Additionally, K-LLVM formulates an abstract machine that executes all LLVM IR instructions. The machine allows to describe our formal semantics in terms of simulating a conceptual virtual machine that runs LLVM IR programs, including non-deterministic programs. Even though the K-LLVM memory model in this paper is assumed to be a sequentially consistent memory model and does not include all LLVM concurrency memory behaviors, the design of K-LLVM’s data layout allows the K-LLVM abstract machine to execute some LLVM IR programs that previous semantics did not cover, such as the full range of LLVM IR behaviors for the interaction among LLVM IR casting, pointer arithmetic, memory operations and some memory flags (e.g. readonly) of function headers. Additionally, the memory model is modularized in a manner that supports investigating other memory models. To validate K-LLVM, we have implemented it in 𝕂 [Roşu, 2016], which generated an interpreter for LLVM IR. Using this, we ran tests including 1,385 unit test programs and around 3,000 concrete LLVM IR programs, and K-LLVM passed all of them.

Cite as

Liyi Li and Elsa L. Gunter. K-LLVM: A Relatively Complete Semantics of LLVM IR. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 7:1-7:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ECOOP.2020.7,
  author =	{Li, Liyi and Gunter, Elsa L.},
  title =	{{K-LLVM: A Relatively Complete Semantics of LLVM IR}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{7:1--7:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.7},
  URN =		{urn:nbn:de:0030-drops-131649},
  doi =		{10.4230/LIPIcs.ECOOP.2020.7},
  annote =	{Keywords: LLVM, formal semantics, K framework, memory model, abstract machine}
}
Document
Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle

Authors: Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle.

Cite as

Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry. Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2019.13,
  author =	{Chen, Ran and Cohen, Cyril and L\'{e}vy, Jean-Jacques and Merz, Stephan and Th\'{e}ry, Laurent},
  title =	{{Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.13},
  URN =		{urn:nbn:de:0030-drops-110683},
  doi =		{10.4230/LIPIcs.ITP.2019.13},
  annote =	{Keywords: Mathematical logic, Formal proof, Graph algorithm, Program verification}
}
Document
Binary-Compatible Verification of Filesystems with ACL2

Authors: Mihir Parang Mehta and William R. Cook

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
Filesystems are an essential component of most computer systems. Work on the verification of filesystem functionality has been focused on constructing new filesystems in a manner which simplifies the process of verifying them against specifications. This leaves open the question of whether filesystems already in use are correct at the binary level. This paper introduces LoFAT, a model of the FAT32 filesystem which efficiently implements a subset of the POSIX filesystem operations, and HiFAT, a more abstract model of FAT32 which is simpler to reason about. LoFAT is proved to be correct in terms of refinement of HiFAT, and made executable by enabling the state of the model to be written to and read from FAT32 disk images. EqFAT, an equivalence relation for disk images, considers whether two disk images contain the same directory tree modulo reordering of files and implementation-level details regarding cluster allocation. A suite of co-simulation tests uses EqFAT to compare the operation of existing FAT32 implementations to LoFAT and check the correctness of existing implementations of FAT32 such as the mtools suite of programs and the Linux FAT32 implementation. All models and proofs are formalized and mechanically verified in ACL2.

Cite as

Mihir Parang Mehta and William R. Cook. Binary-Compatible Verification of Filesystems with ACL2. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{mehta_et_al:LIPIcs.ITP.2019.25,
  author =	{Mehta, Mihir Parang and Cook, William R.},
  title =	{{Binary-Compatible Verification of Filesystems with ACL2}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25},
  URN =		{urn:nbn:de:0030-drops-110807},
  doi =		{10.4230/LIPIcs.ITP.2019.25},
  annote =	{Keywords: interactive theorem proving, filesystems}
}
Document
Robustness Against Transactional Causal Consistency

Authors: Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Distributed storage systems and databases are widely used by various types of applications. Transactional access to these storage systems is an important abstraction allowing application programmers to consider blocks of actions (i.e., transactions) as executing atomically. For performance reasons, the consistency models implemented by modern databases are weaker than the standard serializability model, which corresponds to the atomicity abstraction of transactions executing over a sequentially consistent memory. Causal consistency for instance is one such model that is widely used in practice. In this paper, we investigate application-specific relationships between several variations of causal consistency and we address the issue of verifying automatically if a given transactional program is robust against causal consistency, i.e., all its behaviors when executed over an arbitrary causally consistent database are serializable. We show that programs without write-write races have the same set of behaviors under all these variations, and we show that checking robustness is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. A surprising corollary of the latter result is that causal consistency variations which admit incomparable sets of behaviors admit comparable sets of robust programs. This reduction also opens the door to leveraging existing methods and tools for the verification of concurrent programs (assuming sequential consistency) for reasoning about programs running over causally consistent databases. Furthermore, it allows to establish that the problem of checking robustness is decidable when the programs executed at different sites are finite-state.

Cite as

Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. Robustness Against Transactional Causal Consistency. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{beillahi_et_al:LIPIcs.CONCUR.2019.30,
  author =	{Beillahi, Sidi Mohamed and Bouajjani, Ahmed and Enea, Constantin},
  title =	{{Robustness Against Transactional Causal Consistency}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.30},
  URN =		{urn:nbn:de:0030-drops-109321},
  doi =		{10.4230/LIPIcs.CONCUR.2019.30},
  annote =	{Keywords: Distributed Databases, Causal Consistency, Model Checking}
}
Document
Invited Talk
Petri Net Reachability Problem (Invited Talk)

Authors: Jérôme Leroux

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. In this presentation, we overview decidability and complexity results over the last fifty years about the Petri net reachability problem.

Cite as

Jérôme Leroux. Petri Net Reachability Problem (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{leroux:LIPIcs.MFCS.2019.5,
  author =	{Leroux, J\'{e}r\^{o}me},
  title =	{{Petri Net Reachability Problem}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{5:1--5:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.5},
  URN =		{urn:nbn:de:0030-drops-109493},
  doi =		{10.4230/LIPIcs.MFCS.2019.5},
  annote =	{Keywords: Petri net, Reachability problem, Formal verification, Concurrency}
}
Document
The Next 700 Semantics: A Research Challenge

Authors: Shriram Krishnamurthi, Benjamin S. Lerner, and Liam Elberty

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)


Abstract
Modern systems consist of large numbers of languages, frameworks, libraries, APIs, and more. Each has characteristic behavior and data. Capturing these in semantics is valuable not only for understanding them but also essential for formal treatment (such as proofs). Unfortunately, most of these systems are defined primarily through implementations, which means the semantics needs to be learned. We describe the problem of learning a semantics, provide a structuring process that is of potential value, and also outline our failed attempts at achieving this so far.

Cite as

Shriram Krishnamurthi, Benjamin S. Lerner, and Liam Elberty. The Next 700 Semantics: A Research Challenge. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{krishnamurthi_et_al:LIPIcs.SNAPL.2019.9,
  author =	{Krishnamurthi, Shriram and Lerner, Benjamin S. and Elberty, Liam},
  title =	{{The Next 700 Semantics: A Research Challenge}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{9:1--9:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.9},
  URN =		{urn:nbn:de:0030-drops-105522},
  doi =		{10.4230/LIPIcs.SNAPL.2019.9},
  annote =	{Keywords: Programming languages, desugaring, semantics, testing}
}
Document
Static Analysis for Asynchronous JavaScript Programs

Authors: Thodoris Sotiropoulos and Benjamin Livshits

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Asynchrony has become an inherent element of JavaScript, as an effort to improve the scalability and performance of modern web applications. To this end, JavaScript provides programmers with a wide range of constructs and features for developing code that performs asynchronous computations, including but not limited to timers, promises, and non-blocking I/O. However, the data flow imposed by asynchrony is implicit, and not always well-understood by the developers who introduce many asynchrony-related bugs to their programs. Worse, there are few tools and techniques available for analyzing and reasoning about such asynchronous applications. In this work, we address this issue by designing and implementing one of the first static analysis schemes capable of dealing with almost all the asynchronous primitives of JavaScript up to the 7th edition of the ECMAScript specification. Specifically, we introduce the callback graph, a representation for capturing data flow between asynchronous code. We exploit the callback graph for designing a more precise analysis that respects the execution order between different asynchronous functions. We parameterize our analysis with one novel context-sensitivity flavor, and we end up with multiple analysis variations for building callback graph. We performed a number of experiments on a set of hand-written and real-world JavaScript programs. Our results show that our analysis can be applied to medium-sized programs achieving 79% precision, on average. The findings further suggest that analysis sensitivity is beneficial for the vast majority of the benchmarks. Specifically, it is able to improve precision by up to 28.5%, while it achieves an 88% precision on average without highly sacrificing performance.

Cite as

Thodoris Sotiropoulos and Benjamin Livshits. Static Analysis for Asynchronous JavaScript Programs. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 8:1-8:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{sotiropoulos_et_al:LIPIcs.ECOOP.2019.8,
  author =	{Sotiropoulos, Thodoris and Livshits, Benjamin},
  title =	{{Static Analysis for Asynchronous JavaScript Programs}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{8:1--8:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.8},
  URN =		{urn:nbn:de:0030-drops-108007},
  doi =		{10.4230/LIPIcs.ECOOP.2019.8},
  annote =	{Keywords: static analysis, asynchrony, JavaScript}
}
Document
Transferring Obligations Through Synchronizations

Authors: Jafar Hamin and Bart Jacobs

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only performs the actions for which it has permissions and it also fulfills all of its obligations before it terminates. Although permissions can be transferred through synchronizations from a sender thread, where for example a message is sent or a condition variable is notified, to a receiver thread, where that message or that notification is received, in existing approaches obligations can only be transferred when a thread is forked. In this paper we introduce two mechanisms, one for channels and the other for condition variables, that allow obligations, along with permissions, to be transferred from the sender to the receiver, while ensuring that there is no state where the transferred obligations are lost, i.e. where they are discharged from the sender thread but not loaded onto the receiver thread yet. We show how these mechanisms can be used to modularly verify deadlock-freedom of a number of interesting programs, such as some variations of client-server programs, fair readers-writers locks, and dining philosophers, which cannot be modularly verified without such transfer. We also encoded the proposed separation logic-based proof rules in the VeriFast program verifier and succeeded in verifying the mentioned programs.

Cite as

Jafar Hamin and Bart Jacobs. Transferring Obligations Through Synchronizations. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 19:1-19:58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{hamin_et_al:LIPIcs.ECOOP.2019.19,
  author =	{Hamin, Jafar and Jacobs, Bart},
  title =	{{Transferring Obligations Through Synchronizations}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{19:1--19:58},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.19},
  URN =		{urn:nbn:de:0030-drops-108113},
  doi =		{10.4230/LIPIcs.ECOOP.2019.19},
  annote =	{Keywords: Hoare logic, separation logic, modular program verification, synchronization, transferring obligations, deadlock-freedom}
}
Document
A Program Logic for First-Order Encapsulated WebAssembly

Authors: Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strong guarantees given by WebAssembly’s type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly’s uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly.

Cite as

Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner. A Program Logic for First-Order Encapsulated WebAssembly. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 9:1-9:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{watt_et_al:LIPIcs.ECOOP.2019.9,
  author =	{Watt, Conrad and Maksimovi\'{c}, Petar and Krishnaswami, Neelakantan R. and Gardner, Philippa},
  title =	{{A Program Logic for First-Order Encapsulated WebAssembly}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{9:1--9:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.9},
  URN =		{urn:nbn:de:0030-drops-108011},
  doi =		{10.4230/LIPIcs.ECOOP.2019.9},
  annote =	{Keywords: WebAssembly, program logic, separation logic, soundness, mechanisation}
}
  • Refine by Author
  • 9 Gardner, Philippa
  • 4 Maksimović, Petar
  • 2 Fragoso Santos, José
  • 2 Keil, Matthias
  • 2 König, Barbara
  • Show More...

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

  • Refine by Keyword
  • 5 JavaScript
  • 4 graph transformation
  • 3 separation logic
  • 2 DOM
  • 2 Events
  • Show More...

  • Refine by Type
  • 25 document

  • Refine by Publication Year
  • 8 2019
  • 5 2015
  • 4 2005
  • 4 2020
  • 2 2022
  • Show More...

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