Yu-Fang Chen
Ondřej Lengál
ABSTRACT
We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning an approximate regular model of the set of feasible paths in a program, and testing whether this model contains an incorrect behavior. Exact learning algorithms require checking equivalence between the model and the program, which is a difficult problem, in general undecidable. Our learning procedure is therefore based on the framework of probably approximately correct (PAC) learning, which uses sampling instead, and provides correctness guarantees expressed using the terms error probability and confidence. Besides the verification result, our procedure also outputs the model with the said correctness guarantees. Obtained preliminary experiments show encouraging results, in some cases even outperforming mature software verifiers.
- Software verification competition 2015. http://sv-comp.sosy-lab.org/2015/.Google Scholar
- Dana Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87--106, 1987. Google ScholarDigital Library
- Dana Angluin. Queries and concept learning. Machine Learning, 2(4):319--342, 1987. Google ScholarDigital Library
- Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A tool for configurable software verification. In Proc. of CAV'11, pages 184--190. Springer, 2011. Google ScholarDigital Library
- Benedikt Bollig, Peter Habermehl, Carsten Kern, and Martin Leucker. Angluin-style learning of NFA. In Proc. of IJCAI'09, pages 1004--1009. IJCAI, 2009. Google ScholarDigital Library
- Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider, and David R. Piegdon. libalf: The automata learning framework. In Proc. of CAV'10, volume 6174 of LNCS, pages 360--364. Springer, 2010. Google ScholarDigital Library
- Jacob Burnim and Koushik Sen. Heuristics for scalable dynamic test generation. In Proc. of ASE'08, pages 443--446. IEEE Computer Society, 2008. Google ScholarDigital Library
- Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, and Michael Tautschnig. Learning the language of error. In Proc. of ATVA'15, volume 9364 of LNCS, pages 114--130. Springer, 2015.Google ScholarCross Ref
- Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, and Bow-Yaw Wang. Learning minimal separating DFA's for compositional verification. In Proc. of TACAS'09, volume 5505 of LNCS, pages 31--45. Springer, 2009. Google ScholarDigital Library
- Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Proc. of TACAS'04, volume 2988 of LNCS, pages 168--176. Springer, 2004.Google ScholarCross Ref
- Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. Pasareanu. Learning assumptions for compositional verification. In Proc. of TACAS'03, volume 2619 of LNCS, pages 331--346. Springer, 2003. Google ScholarDigital Library
- Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: directed automated random testing. In Proc. of PLDI'05, pages 213--223. ACM, 2005. Google ScholarDigital Library
- Oded Goldreich, Shari Goldwasser, and Dana Ron. Property testing and its connection to learning and approximation. Journal of ACM, 45(4):653--750, July 1998. Google ScholarDigital Library
- Michael J. Kearns and Umesh Virkumar Vazirani. An introduction to computational learning theory. MIT Press, 1994. Google ScholarDigital Library
- Axel Legay, Benoît Delahaye, and Saddek Bensalem. Statistical model checking: An overview. In Proc. of RV'10, volume 6418 of LNCS, pages 122--135. Springer, 2010. Google ScholarDigital Library
- Oliver Matz, Axel Miller, Andreas Potthoff, Wolfgang Thomas, and Erich Valkema. Report on the program AMoRE. 1995.Google Scholar
- George C. Necula, Scott McPeak, Shree Prakash Rahul, and Westley Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Proc. of CC'02, volume 2304 of LNCS, pages 213--228. Springer, 2002. Google ScholarDigital Library
- Ronald L. Rivest and Robert E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 103(2):299--347, 1993. Google ScholarDigital Library
- Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for C. In Proc. of FSE'05, pages 263--272. ACM, 2005. Google ScholarDigital Library
- Koushik Sen, Mahesh Viswanathan, and Gul Agha. Statistical model checking of black-box probabilistic systems. In Proc. of CAV'04, volume 3114 of LNCS, pages 202--215. Springer, 2004.Google ScholarCross Ref
- Leslie G. Valiant. A theory of the learnable. Communications of the ACM, 27(11):1134--1142, 1984. Google ScholarDigital Library
- Neil Walkinshaw. Assessing test adequacy for black-box systems without specifications. In Proc. of ICTSS'11, volume 7019 of LNCS, pages 209--224. Springer, 2011. Google ScholarDigital Library
- Paolo Zuliani, André Platzer, and Edmund M. Clarke. Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods in System Design, 43(2):338--367, 2013. Google ScholarDigital Library
- PAC learning-based verification and model synthesis
Recommendations
Model-based Runtime Verification Framework for Self-optimizing Systems
This paper describes a novel on-line model checking approach offered as service of a real-time operating system (RTOS). The verification system is intended especially for self-optimizing component-based real-time systems where self-optimization is ...
Model-based Runtime Verification Framework
Model-based runtime verification is an extension to the state-of-the-art runtime verification, aimed at checking at runtime the system implementation against the system model (consistency checking) and the system model against the system specification (...
Compositional verification by model checking for counter-examples
ISSTA '96: Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysisMany concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using model checking. In this approach an abstract, finite-state model of ...
Comments