License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.8.2.12
URN: urn:nbn:de:0030-drops-162105
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16210/
Go back to Dagstuhl Artifacts Series


Grannan, Zachary ; Vazou, Niki ; Darulova, Eva ; Summers, Alexander J.

REST: Integrating Term Rewriting with Program Verification (Artifact)

pdf-format:
DARTS-8-2-12.pdf (0.5 MB)
artifact-format:
DARTS-8-2-12-artifact-4c74c72ab1072f56789e9a9f112abac2.gz.tar (4,002 MB)

Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy.


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).

BibTeX - Entry

@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/opus/volltexte/2022/16210},
  URN =		{urn:nbn:de:0030-drops-162105},
  doi =		{10.4230/DARTS.8.2.12},
  annote =	{Keywords: term rewriting, program verification, theorem proving}
}

Keywords: term rewriting, program verification, theorem proving
Collection: DARTS, Volume 8, Issue 1, Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)
Issue Date: 2022
Date of publication: 23.06.2022


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI