CiMPG plus F: A Proof Generator and Fixer-Upper for CafeOBJ Specifications

被引：7

作者：

Riesco, Adrian ^{[1
]}

Ogata, Kazuhiro ^{[2
,3
]}

机构：

[1] Univ Complutense Madrid, Fac Informat, Madrid, Spain

[2] JAIST, Sch Informat Sci, Nomi, Japan

[3] JAIST, Res Ctr Theoret Comp Sci, Nomi, Japan

来源：

THEORETICAL ASPECTS OF COMPUTING, ICTAC 2020 | 2020年 / 12545卷

关键词：

CafeOBJ; Theorem Proving; Automatic Proof Inference;

D O I：

10.1007/978-3-030-64276-1_4

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

CafeOBJ is a language for writing formal specifications of software and hardware systems. It implements equational logic by rewriting and has been used to verify properties of systems using both proof scores and theorem proving. In this paper, we present CiMPG+F, an extension of the CafeInMaude interpreter that, for a large class of CafeOBJ specifications, (i) generates complete proofs from scratch and (ii) fixes incomplete proof scores. CiMPG+F allowed us to prove from scratch the correctness of different protocols, giving us confidence in the approach.

引用

页码：64 / 82

页数：19