Checking Zenon Modulo Proofs in Dedukti

被引：8
|
作者：
Cauderlier, Raphael [1 ]
Halmagrand, Pierre [1 ]
机构：
[1] Cnam Inria, Paris, France
来源：
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2015年 / 186期
关键词：
D O I：
10.4204/EPTCS.186.7
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Dedukti has been proposed as a universal proof checker. It is a logical framework based on the. lambda Pi-calculus modulo that is used as a backend to verify proofs coming from theorem provers, especially those implementing some form of rewriting. We present a shallow embedding into Dedukti of proofs produced by Zenon Modulo, an extension of the tableau-based first-order theorem prover Zenon to deduction modulo and typing. Zenon Modulo is applied to the verification of programs in both academic and industrial projects. The purpose of our embedding is to increase the confidence in automatically generated proofs by separating untrusted proof search from trusted proof verification.
引用
收藏
页码：57 / 73
页数：17
相关论文
共 50 条
  • [31] Proofs about folklore: Why model checking = reachability?
    Choe, K.
    Eo, H.
    O, S.
    Shilov, N. V.
    Yi, K.
    MATHEMATICAL LOGIC IN ASIA, 2006, : 41 - +
  • [32] Zero knowledge Proofs for Cloud Storage Integrity Checking
    Zhang, Faen
    Fan, Xinyu
    Lei, Xiang
    Wu, Jiahong
    Song, Jianfei
    Huang, Jiashui
    Guo, Jingming
    Tong, Chao
    PROCEEDINGS OF THE 39TH CHINESE CONTROL CONFERENCE, 2020, : 7661 - 7668
  • [33] Proofs of Data Possession and Pollution Checking for Regenerating Codes
    Corena, Juan Camilo
    Ohtsuki, Tomoaki
    2013 IEEE GLOBAL COMMUNICATIONS CONFERENCE (GLOBECOM), 2013, : 2717 - 2722
  • [34] Certifying proofs for SAT-based model checking
    Alberto Griggio
    Marco Roveri
    Stefano Tonetta
    Formal Methods in System Design, 2021, 57 : 178 - 210
  • [35] Integrating Topological Proofs with Model Checking to Instrument Iterative Design
    Menghi, Claudio
    Rizzi, Alessandro Maria
    Bernasconi, Anna
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2020), 2020, 12076 : 53 - 74
  • [36] Evidence explorer: A tool for exploring model-checking proofs
    Dong, YF
    Ramakrishnan, CR
    Smolka, SA
    COMPUTER AIDED VERIFICATION, 2003, 2725 : 215 - 218
  • [37] Cooperative Set Homomorphic Proofs for Data Possession Checking in Clouds
    Kaaniche, Nesrine
    Laurent, Maryline
    Canard, Sebastien
    IEEE TRANSACTIONS ON CLOUD COMPUTING, 2021, 9 (01) : 102 - 117
  • [38] Electrical Rule Checking of Integrated Circuits using Satisfiability Modulo Theory
    Ferres, B.
    Oulkaid, O.
    Henrio, L.
    Khosravian, M. G.
    Moy, M.
    Radanne, G.
    Raymond, P.
    2023 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION, DATE, 2023,
  • [39] Goal-Directed Invariant Synthesis for Model Checking Modulo Theories
    Ghilardi, Silvio
    Ranise, Silvio
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, PROCEEDINGS, 2009, 5607 : 173 - +
  • [40] Fairness Modulo Theory: A New Approach to LTL Software Model Checking
    Dietsch, Daniel
    Heizmann, Matthias
    Langenfeld, Vincent
    Podelski, Andreas
    COMPUTER AIDED VERIFICATION, PT I, 2015, 9206 : 49 - 66
12345