Instrumenting a weakest precondition calculus for counterexample generation

被引：11

作者：

Dailler, Sylvain ^{[1
,2
,3
]}

Hauzar, David ^{[1
,2
,3
,4
]}

Marche, Claude ^{[1
,2
,3
]}

Moy, Yannick ^{[4
]}

机构：

[1] Univ Paris Saclay, INRIA, F-91120 Palaiseau, France

[2] CNRS, LRI, F-91405 Orsay, France

[3] Univ Paris Sud, F-91405 Orsay, France

[4] AdaCore, F-75009 Paris, France

来源：

JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING | 2018年 / 99卷

关键词：

Deductive program verification; Weakest precondition calculus; Satisfiability modulo theories; Counterexamples; VERIFICATION;

D O I：

10.1016/j.jlamp.2018.05.003

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

A major issue in the activity of deductive program verification is to understand why automated provers fail to discharge a proof obligation. To help the user understand the problem and decide what needs to be fixed in the code or the specification, it is essential to provide means to investigate such a failure. We present our approach for the design and the implementation of counterexample generation, exhibiting values for the variables of the program where a given part of the specification fails to be validated. To produce a counterexample, we exploit the ability of SMT solvers to propose, when a proof of a formula is not found, a counter-model. Turning such a counter-model into a counterexample for the initial program is not trivial because of the many transformations leading from a particular piece of code and its specification to a set of proof goals given to external provers. (C) 2018 Elsevier Inc. All rights reserved.

引用

页码：97 / 113

页数：17

共 33 条

[1]

[Anonymous], LECT NOTES COMPUTER

[2]

Barnes John., 2014, PROGRAMMING ADA 2012

[3]

Barnett M, 2006, LECT NOTES COMPUT SC, V4111, P364

[4]

Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14

[5]

Barrett Clark, 2010, P 8 INT WORKSH SAT M

[6]

Blanchette JC, 2010, LECT NOTES COMPUT SC, V6172, P131, DOI 10.1007/978-3-642-14052-5_11

[7]

Bobot F., 2011, BOOGIE 2011 1 INT WO, P53

[8] Let's verify this with Why3 [J].

Bobot, Francois ;

Filliatre, Jean-Christophe ;

Marche, Claude ;

Paskevich, Andrei .

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2015, 17 (06) :709-727

[9]

Bobot Francois, 2008, The Alt-Ergo automated theorem prover

[10]

Chapman Roderick, 2014, Interactive Theorem Proving. 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Proceedings: LNCS 8558, P17, DOI 10.1007/978-3-319-08970-6_2

← 1 2 3 4 →