DROPS

Document

Artifact

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}
}

Search Results

Documents authored by Vazou, Niki

REST: Integrating Term Rewriting with Program Verification (Artifact)

Abstract

Cite as

REST: Integrating Term Rewriting with Program Verification

Abstract

Cite as

Thanks for your feedback!

Could not send message