Encoding TLA plus proof obligations safely for SMT

被引：0
作者：
Defourne, Rosalie [1 ]
机构：
[1] Univ Lorraine, CNRS, Inria, LORIA, Nancy, France
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2025年 / 239卷
基金：
欧洲研究理事会;
关键词：
Automated theorem proving; SMT; TLA plus; TLAPS;
D O I：
10.1016/j.scico.2024.103178
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The TLA+ + Proof System (TLAPS) allows users to verify proofs with the support of automated theorem provers, including SMT solvers. To increase trust in TLAPS, we revisited the encoding of TLA+ + for SMT, 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.
引用
收藏
页数：32
相关论文
共 32 条
  • [1] Abrial J.R., 1996, The B-Book-Assigning Programs to Meanings
  • [2] Baaz M., 2001, Handbook of Automated Reasoning, V1, P273
  • [3] cvc5: A Versatile and Industrial-Strength SMT Solver
    Barbosa, Haniel
    Barrett, Clark
    Brain, Martin
    Kremer, Gereon
    Lachnitt, Hanna
    Mann, Makai
    Mohamed, Abdalrhman
    Mohamed, Mudathir
    Niemetz, Aina
    Notzli, Andres
    Ozdemir, Alex
    Preiner, Mathias
    Reynolds, Andrew
    Sheng, Ying
    Tinelli, Cesare
    Zohar, Yoni
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 : 415 - 442
  • [4] Extending SMT Solvers to Higher-Order Logic
    Barbosa, Haniel
    Reynolds, Andrew
    El Ouraoui, Daniel
    Tinelli, Cesare
    Barrett, Clark
    [J]. AUTOMATED DEDUCTION, CADE 27, 2019, 11716 : 35 - 54
  • [5] Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14
  • [6] Bobot F., 2011, Boogie 2011, P53
  • [7] Zenon: An extensible automated theorem prover producing checkable proofs
    Bonichon, Richard
    Delahaye, David
    Doligez, Damien
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2007, 4790 : 151 - +
  • [8] Bouton T, 2009, LECT NOTES ARTIF INT, V5663, P151, DOI 10.1007/978-3-642-02959-2_12
  • [9] Danvy Olivier, 2001, PPDP '01, P162, DOI DOI 10.1145/773184.773202
  • [10] Z3: An efficient SMT solver
    de Moura, Leonardo
    Bjorner, Nikolaj
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
1234