SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques
作者： Edmund Clarke , Anubhav Gupta , James Kukula , Ofer Strichman
关键词: Model checking 、 Abstraction (linguistics) 、 Machine learning 、 Constraint satisfaction 、 Computer science 、 Artificial intelligence 、 Boolean satisfiability problem 、 Integer programming 、 Counterexample 、 Propositional calculus 、 Linear programming
摘要: We describe new techniques for model checking in the counterexample guided abstraction/refinement framework. The abstraction phase 'hides' logic of various variables, hence considering them as inputs. This type may lead to 'spurious' counterexamples, i.e. traces that can not be simulated on original (concrete) machine. check whether a is real or spurious with SAT checker. then use combination Integer Linear Programming (ILP) and machine learning refining based counterexample. process repeated until either found property verified.We have implemented these top checker NuSMV solver Chaff. Experimental results prove viability techniques.
springer.com
core.ac.uk
acm.org
sci-hub.st 参考文章(15)
Steven L. Salzberg, Alberto Segre, Programs for Machine Learning ,(1994)
Felice Balarin, Alberto L. Sangiovanni-Vincentelli, An Iterative Approach to Language Containment computer aided verification. pp. 29- 40 ,(1993) , 10.1007/3-540-56922-7_4
Jørn Lind-Nielsen, Henrik Reif Andersen, Stepwise CTL Model Checking of State/Event Systems computer aided verification. pp. 316- 327 ,(1999) , 10.1007/3-540-48683-6_28
A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri, NUSMV: A New Symbolic Model Verifier computer aided verification. ,vol. 1633, pp. 495- 499 ,(1999) , 10.1007/3-540-48683-6_44
Robert P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach ,(1995)
Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu, Symbolic Model Checking without BDDs tools and algorithms for construction and analysis of systems. pp. 193- 207 ,(1999) , 10.1007/3-540-49059-0_14
Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, Marco Roveri, NUSMV: a new symbolic model checker International Journal on Software Tools for Technology Transfer. ,vol. 2, pp. 410- 425 ,(2000) , 10.1007/S100090050046
Edmund M. Clarke, Orna Grumberg, David E. Long, Model checking and abstraction ACM Transactions on Programming Languages and Systems. ,vol. 16, pp. 1512- 1542 ,(1994) , 10.1145/186025.186051
Dong Wang, Pei-Hsin Jiang, James Kukula, Yunshan Zhu, Tony Ma, Robert Damiano, None, Formal property verification by abstraction refinement with formal, simulation and hybrid engines design automation conference. pp. 35- 40 ,(2001) , 10.1145/378239.378260
J. Ross Quinlan, C4.5: Programs for Machine Learning ,(1992)