Dirk Beyer
Stefan Löwe
Philipp Wendler
ABSTRACT
Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.
- J. Backes, S. Person, N. Rungta, and O. Tkachuk. Regression verification using impact summaries. In Proc. SPIN, LNCS 7976, pp. 99–116. Springer, 2013.Google Scholar
- T. Ball and S. K. Rajamani. The Slam project: Debugging system software via static analysis. In Proc. POPL, pp. 1–3. ACM, 2002. Google ScholarDigital Library
- C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0. In Proc. SMT, 2010.Google Scholar
- D. Beyer. Second competition on software verification (Summary of SV-COMP 2013). In Proc. TACAS, LNCS 7795, pp. 594–609. Springer, 2013. Google ScholarDigital Library
- D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software model checking via large-block encoding. In Proc. FMCAD, pp. 25–32. IEEE, 2009.Google Scholar
- D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker Blast. Int. J. Softw. Tools Technol. Transfer, 9(5-6):505–525, 2007. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, M. E. Keremoglu, and P. Wendler. Conditional model checking: A technique to pass information between verifiers. In Proc. FSE. ACM, 2012. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, and G. Théoduloz. Lazy shape analysis. In Proc. CAV, LNCS 4144, pp. 532–546. Springer, 2006. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, and G. Théoduloz. Program analysis with dynamic precision adjustment. In Proc. ASE, pp. 29–38. IEEE, 2008. Google ScholarDigital Library
- D. Beyer, A. Holzer, M. Tautschnig, and H. Veith. Information reuse for multi-goal reachability analyses. In Proc. ESOP, pp. 472–491. Springer, 2013. Google ScholarDigital Library
- D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In Proc. CAV, LNCS 6806, pp. 184–190. Springer, 2011. Google ScholarDigital Library
- D. Beyer, M. E. Keremoglu, and P. Wendler. Predicate abstraction with adjustable-block encoding. In Proc. FMCAD, pp. 189–197. FMCAD, 2010. Google ScholarDigital Library
- D. Beyer and S. Löwe. Explicit-state software model checking based on CEGAR and interpolation. In Proc. FASE, LNCS 7793, pp. 146–162. Springer, 2013. Google ScholarDigital Library
- D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, and P. Wendler. Reusing precisions for efficient regression verification. Technical Report MIP-1302, University of Passau, 2013. http://arxiv.org/abs/1305.6915.Google Scholar
- D. Beyer and A. K. Petrenko. Linux driver verification. In Proc. ISoLA, LNCS 7610, pp. 1–6. Springer, 2012. Google ScholarDigital Library
- D. Beyer and P. Wendler. Reuse of verification results: Conditional model checking, precision reuse, and verification witnesses. In Proc. SPIN, LNCS 7976, pp. 1–17. Springer, 2013.Google ScholarCross Ref
- M. Böhme, B. C. d. S. Oliveira, and A. Roychoudhury. Partition-based regression verification. In Proc. ICSE. IEEE, 2013. Google ScholarDigital Library
- S. Chaki, A. Gurfinkel, and O. Strichman. Regression verification for multi-threaded programs. In Proc. VMCAI, pp. 119–135. Springer, 2012. Google ScholarDigital Library
- H. Chockler, A. Ivrii, A. Matsliah, S. Moran, and Z. Nevo. Incremental formal verification of hardware. In Proc. FMCAD, pp. 135–143. FMCAD, 2011. Google ScholarDigital Library
- M. Christakis, P. Müller, and V. Wüstholz. Collaborative verification and testing with explicit assumptions. In Proc. FM, pp. 132–146, 2012.Google ScholarCross Ref
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752–794, 2003. Google ScholarDigital Library
- B. Godlin and O. Strichman. Regression verification: Proving the equivalence of similar programs. Software Testing, Verification, and Reliability, 2009.Google Scholar
- S. Graf and H. Sa¨ıdi. Construction of abstract state graphs with Pvs. In CAV, pp. 72–83. Springer, 1997. Google ScholarDigital Library
- T. L. Graves, M. J. Harrold, J.-M. Kim, A. A. Porter, and G. Rothermel. An empirical study of regression test selection techniques. In Proc. ICSE, pp. 188–197. IEEE, 1998. Google ScholarDigital Library
- R. H. Hardin, R. P. Kurshan, K. L. McMillan, J. A. Reeds, and N. J. A. Sloane. Efficient regression verification. In Proc. WODES, pp. 147–150, 1996.Google Scholar
- T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In Proc. POPL, pp. 232–244. ACM, 2004. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and M. A. A. Sanvido. Extreme model checking. In Proc. Verification: Theory and Practice, LNCS 2772, pp. 332–358. Springer, 2003.Google Scholar
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, pp. 58–70. ACM, 2002. Google ScholarDigital Library
- A. V. Khoroshilov, V. S. Mutilin, A. K. Petrenko, and V. Zakharov. Establishing Linux driver verification process. In Proc. Ershov Memorial Conference, LNCS 5947, pp. 165–176. Springer, 2009. Google ScholarDigital Library
- S. Lauterburg, A. Sobeih, D. Marinov, and M. Viswanathan. Incremental state-space exploration for programs with dynamically allocated data. In Proc. ICSE, pp. 291–300. ACM, 2008. Google ScholarDigital Library
- M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. V. Khoroshilov, and P. E. Shved. Using Linux device drivers for static verification tools benchmarking. Programming and Comp. Softw., 38(5):245–256, 2012. Google ScholarDigital Library
- G. J. Myers. The Art of Software Testing. Wiley, 1979. Google ScholarDigital Library
- S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed incremental symbolic execution. ACM SIGPLAN Notices, 46(6):504–515, 2011. Google ScholarDigital Library
- G. Rothermel and M. J. Harrold. Analyzing regression test selection techniques. IEEE Trans. Softw. Eng., 22(8):529–551, 1996. Google ScholarDigital Library
- O. Sery, G. Fedyukovich, and N. Sharygina. Incremental upgrade checking by means of interpolation-based function summaries. In Proc. FMCAD, pp. 114–121. FMCAD, 2012.Google Scholar
- O. V. Sokolsky and S. A. Smolka. Incremental model checking in the modal mu-calculus. In Proc. CAV, LNCS 818, pp. 351–363. Springer, 1994. Google ScholarDigital Library
- O. Strichman and B. Godlin. Regression verification — a practical way to verify programs. In Proc. Verified Software: Theories, Tools, Experiments, pp. 496–501. Springer, 2008. Google ScholarDigital Library
- W. Visser, J. Geldenhuys, and M. B. Dwyer. Green: Reducing, reusing, and recycling constraints in program analysis. In Proc. FSE. ACM, 2012. Google ScholarDigital Library
- G. Yang, M. B. Dwyer, and G. Rothermel. Regression model checking. In ICSM, pp. 115–124. IEEE, 2009.Google Scholar
- G. Yang, C. S. Păsăreanu, and S. Khurshid. Memoized symbolic execution. In ISSTA, pp. 144–154. 2012. Google ScholarDigital Library
Index Terms
- Precision reuse for efficient regression verification
Recommendations
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Compositional reachability analysis for efficient modular verification of asynchronous designs
Compositional verification is essential to address state explosion in model checking. Traditionally, an over-approximate context is needed for each individual component in a system for sound verification. This may cause state explosion for the ...
Coverage metrics for formal verification
In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors of ...
Comments