Encoding rmTLA+ Proof Obligations Safely for SMT

Rosalie Defourné
Digital Printed Abstract View Cite
Type
Conference paper
Publication
9th International Conference on Rigorous State Based Methods (ABZ'23)

Abstract

The (\textrm{TLA}^{+}) Proof System (TLAPS) allows users to verify proofs with the support of automated provers, including SMT solvers. To better ensure the soundness of TLAPS, we revisited the encoding of (\textrm{TLA}^{+}) into SMT-LIB, whose implementation had become too complex. Our approach is based on a first-order axiomatization with E-matching patterns. The new encoding is available with TLAPS and achieves performances similar to the previous version, despite its simpler design.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Defourne23,
  author       = {Rosalie Defourn{\'{e}}},
  editor       = {Uwe Gl{\"{a}}sser and
                  Jos{\'{e}} Creissac Campos and
                  Dominique M{\'{e}}ry and
                  Philippe A. Palanque},
  title        = {Encoding rmTLA\({}^{\mbox{+}}\) Proof Obligations Safely for {SMT}},
  booktitle    = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
                  2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14010},
  pages        = {88--106},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-33163-3\_7},
  doi          = {10.1007/978-3-031-33163-3\_7},
  timestamp    = {Tue, 23 May 2023 09:57:42 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/Defourne23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'23

Related