Search Results

Documents authored by Summers, Alexander J.

Document
Artifact
DOI: 10.4230/DARTS.8.2.12
REST: Integrating Term Rewriting with Program Verification (Artifact)

Authors: Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
This artifact contains code for REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. The artifact includes the REST library as well as a version of Liquid Haskell extended with REST. In addition, it includes the scripts that were used to generate the tables in the paper’s evaluation section. Also included is a docker image containing a development environment for REST (and the Liquid Haskell extension).
Cite as

Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST: Integrating Term Rewriting with Program Verification (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{grannan_et_al:DARTS.8.2.12,
  author =	{Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
  title =	{{REST: Integrating Term Rewriting with Program Verification (Artifact)}},
  pages =	{12:1--12:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.12},
  URN =		{urn:nbn:de:0030-drops-162105},
  doi =		{10.4230/DARTS.8.2.12},
  annote =	{Keywords: term rewriting, program verification, theorem proving}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.13
REST: Integrating Term Rewriting with Program Verification

Authors: Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively selecting orderings based on the path of rewrites taken so far; and (3) integrating external oracles that allow steps that cannot be justified with rewrite rules. Our REST approach is designed around an easily implementable core algorithm, parameterizable by choices of term orderings and their implementations; in this way our approach can be easily integrated into existing tools. We implemented REST as a Haskell library and incorporated it into Liquid Haskell’s evaluation strategy, extending Liquid Haskell with rewriting rules. We evaluated our REST implementation by comparing it against both existing rewriting techniques and E-matching (as used in most SMT solvers) and by showing that it can be used to supplant manual lemma application in many existing Liquid Haskell proofs.
Cite as

Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST: Integrating Term Rewriting with Program Verification. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 13:1-13:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{grannan_et_al:LIPIcs.ECOOP.2022.13,
  author =	{Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
  title =	{{REST: Integrating Term Rewriting with Program Verification}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{13:1--13:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.13},
  URN =		{urn:nbn:de:0030-drops-162416},
  doi =		{10.4230/LIPIcs.ECOOP.2022.13},
  annote =	{Keywords: term rewriting, program verification, theorem proving}
}
Document
DOI: 10.4230/DARTS.1.1.10
Lightweight Support for Magic Wands in an Automatic Verifier (Artifact)

Authors: Malte Schwerhoff and Alexander J. Summers

Published in: DARTS, Volume 1, Issue 1, Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
This artifact is based on Silicon, which is an automatic verification tool for programs written in the Silver Intermediate Verification Language. Silver is designed to natively support permission-based reasoning, in the style of separation logic and similar approaches. Our extension of Silicon provides support for specification and verification of programs using the magic wand operator, which can be used to represent ways to exchange views on the program state, or to represent partial versions of data structures. Our implementation is a backwards-compatible extension of the basic tool, and is provided along with a test suite of examples and regressions in a VirtualBox image. Instructions for running our tool on these (and user-defined) examples are provided in the image, to allow users to experiment with the verifier.
Cite as

Malte Schwerhoff and Alexander J. Summers. Lightweight Support for Magic Wands in an Automatic Verifier (Artifact). In Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). Dagstuhl Artifacts Series (DARTS), Volume 1, Issue 1, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{schwerhoff_et_al:DARTS.1.1.10,
  author =	{Schwerhoff, Malte and Summers, Alexander J.},
  title =	{{Lightweight Support for Magic Wands in an Automatic Verifier (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2015},
  volume =	{1},
  number =	{1},
  editor =	{Schwerhoff, Malte and Summers, Alexander J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.1.1.10},
  URN =		{urn:nbn:de:0030-drops-55192},
  doi =		{10.4230/DARTS.1.1.10},
  annote =	{Keywords: Magic Wand, Software Verification, Automatic Verifiers, Separation Logic, Implicit Dynamic Frames}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ECOOP.2015.3
Software Verification "Across the Stack" (Invited Talk)

Authors: Alexander J. Summers

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

Abstract
Producing reliable programs has always been tough, and the complexity and variety of programming tasks just keeps on growing. Fortunately, the growth of computing power has also enabled substantial advances in automated reasoning, particularly the development of SMT solvers and automatic theorem provers. In turn, this has resulted in new research directions for program correctness, with the aim of producing tools which can verify complex properties of software automatically. Developing useful verification techniques requires balancing a number of competing factors. We want to be as expressive as possible in the program properties we can support - if we can write it down, we'd like to be able to prove it. But to progress beyond pen-and-paper efforts, we also need to tailor our approaches such that they can be implemented or encoded by tools, ideally with both precise and efficient results. To make things harder still, if we hope to produce tools which everyday programmers can benefit from, we also need techniques that require manageable interaction from a user, and give understandable feedback. In this talk, I'll describe some of the fun experiences I've had working on these kinds of problems, from the design of front-end program logics and reasoning techniques to the development of underlying implementation technology, and the tricky encoding challenges that show up in between.
Cite as

Alexander J. Summers. Software Verification "Across the Stack" (Invited Talk). In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, p. 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{summers:LIPIcs.ECOOP.2015.3,
  author =	{Summers, Alexander J.},
  title =	{{Software Verification "Across the Stack"}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{3--3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.3},
  URN =		{urn:nbn:de:0030-drops-52141},
  doi =		{10.4230/LIPIcs.ECOOP.2015.3},
  annote =	{Keywords: software verification, program logic, automatic verifier, program correctness, SMT solvers}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.614
Lightweight Support for Magic Wands in an Automatic Verifier

Authors: Malte Schwerhoff and Alexander J. Summers

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

Abstract
Permission-based verification logics such as separation logic have led to the development of many practical verification tools over the last decade. Verifiers employ the separating conjunction A*B to elegantly handle aliasing problems, framing, race conditions, etc. Introduced along with the separating conjunction, the magic wand connective, written A -* B, can describe hypothetical modifications of the current state, and provide guarantees about the results. Its formal semantics involves quantifying over states: as such, the connective is typically not supported in automatic verification tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, for example, for specifying loop invariants and partial data structures. In this paper, we show how to integrate support for the magic wand into an automatic verifier, requiring low specification overhead from the tool user, due to a novel approach for choosing footprints for magic wand formulas automatically. We show how to extend this technique to interact elegantly with common specification features such as recursive predicates. Our solution is designed to be compatible with a variety of logics and underlying implementation techniques. We have implemented our approach, and a prototype verifier is available to download, along with a collection of examples.
Cite as

Malte Schwerhoff and Alexander J. Summers. Lightweight Support for Magic Wands in an Automatic Verifier. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 614-638, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schwerhoff_et_al:LIPIcs.ECOOP.2015.614,
  author =	{Schwerhoff, Malte and Summers, Alexander J.},
  title =	{{Lightweight Support for Magic Wands in an Automatic Verifier}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{614--638},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.614},
  URN =		{urn:nbn:de:0030-drops-52408},
  doi =		{10.4230/LIPIcs.ECOOP.2015.614},
  annote =	{Keywords: Magic Wand, Software Verification, Automatic Verifiers, Separation Logic, Implicit Dynamic Frames}
}
Document
DOI: 10.4230/DagSemProc.08061.3
A Unified Framework for Verification Techniques for Object Invariants

Authors: Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers

Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)

Abstract
Object invariants define the consistency of objects. They have subtle semantics, mainly because of call-backs, multi-object invariants, and subclassing. Several verification techniques for object invariants have been proposed. It is difficult to compare these techniques, and to ascertain their soundness, because of their differences in restrictions on programs and invariants, in the use of advanced type systems (e.g., ownership types), in the meaning of invariants, and in proof obligations. We develop a unified framework for such techniques. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters which guarantee soundness. We instantiate our framework with three verification techniques from the literature, and use it to assess soundness and compare expressiveness.
Cite as

Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers. A Unified Framework for Verification Techniques for Object Invariants. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{drossopoulou_et_al:DagSemProc.08061.3,
  author =	{Drossopoulou, Sophia and Francalanza, Adrian and M\"{u}ller, P. and Summers, Alexander J.},
  title =	{{A Unified Framework for  Verification Techniques for Object Invariants}},
  booktitle =	{Types, Logics and Semantics for State},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8061},
  editor =	{Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.3},
  URN =		{urn:nbn:de:0030-drops-14278},
  doi =		{10.4230/DagSemProc.08061.3},
  annote =	{Keywords: Object invariants, visible states semantics, verification, sound}
}
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