Certificates for Parameterized Model Checking

被引:13
作者
Conchon, Sylvain [1 ,2 ]
Mebsout, Alain [2 ,3 ]
Zaidi, Fatiha [1 ]
机构
[1] Univ Paris 11, CNRS, LRI, F-91405 Orsay, France
[2] INRIA Saclay Ile de France, F-91893 Orsay, France
[3] Univ Iowa, Iowa City, IA USA
来源
FM 2015: FORMAL METHODS | 2015年 / 9109卷
关键词
D O I
10.1007/978-3-319-19249-9_9
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper presents a technique for the certification of Cubicle, a model checker for proving safety properties of parameterized systems. To increase the confidence in its results, Cubicle now produces a proof object (or certificate) that, if proven valid, guarantees that the answer for this specific input is correct. The main challenges addressed in this paper are (1) the production of such certificates without degrading the performances of the model checker and (2) the construction of these proof objects so that they can be independently and efficiently verified by an SMT solver. Since the burden of correctness insurance now relies on this external solver, a stronger guarantee is obtained by the use of multiple backend automatic provers for redundancy. Experiments show that our approach does not impact Cubicle's performances and that we were able to verify certificates for challenging parameterized problems. As a byproduct, these certificates allowed us to find subtle and critical implementation bugs in Cubicle.
引用
收藏
页码:126 / 142
页数:17
相关论文
共 30 条
[1]  
Amjad H, 2003, LECT NOTES COMPUT SC, V2758, P171
[2]  
[Anonymous], 2006, Technical Report
[3]  
[Anonymous], 2010, LMCS
[4]  
Armand M., 2011, PSATTT 2011 INT WORK
[5]  
Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14
[6]  
Blazy S, 2013, LECT NOTES COMPUT SC, V7935, P324, DOI 10.1007/978-3-642-38856-9_18
[7]  
Bobot Francois, 2008, The Alt-Ergo automated theorem prover
[8]  
Conchon Sylvain, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P718, DOI 10.1007/978-3-642-31424-7_55
[9]  
Conchon S, 2013, 2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), P61
[10]   Z3: An efficient SMT solver [J].
de Moura, Leonardo ;
Bjorner, Nikolaj .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 :337-340