Document Open Access Logo

REST: Integrating Term Rewriting with Program Verification (Artifact)

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

PDF
Thumbnail PDF

Artifact Description

DARTS.8.2.12.pdf
  • Filesize: 0.49 MB
  • 2 pages

Document Identifiers

Author Details

Zachary Grannan
  • University of British Columbia, Vancouver, Canada
Niki Vazou
  • IMDEA Software Institute, Madrid, Spain
Eva Darulova
  • Uppsala University, Sweden
Alexander J. Summers
  • University of British Columbia, Vancouver, Canada

Funding

This work was supported by the Juan de la Cierva grants IJC2019-041599-I, the HaCrypt ONR project N00014-19-1-2292, and the ERC starting grant CRETE (101039196). We acknowledge the support of the Natural Sciences and Engineering Research Council of Canada (NSERC).

Acknowledgements

We thank Jonathan Chan, Eric Conlon, Rui Ge, Paulette Koronkevich and the anonymous reviewers for their helpful and constructive feedback.

Cite AsGet BibTex

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)
https://doi.org/10.4230/DARTS.8.2.12

Artifact

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

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • term rewriting
  • program verification
  • theorem proving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Article

  • 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), LIPIcs, Vol. 222, pp. 13:1-13:29, 2022. https://doi.org/10.4230/LIPIcs.ECOOP.2022.13
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