ABSTRACT
This paper studies and optimizes automated program verification. Detailed reasoning about software behavior is often facilitated by program invariants that hold across all program executions. Finding program invariants is in fact an essential step in automated program verification. Automatic discovery of precise invariants, however, can be very difficult in practice. The problem can be simplified if one has access to a candidate set of assertions (or annotations) and the search for invariants is limited over the space defined by these annotations. Then, the main challenge is to automatically generate quality program annotations. We present an approach that infers program annotations automatically by leveraging the history of verifying related programs. Our algorithm extracts high-quality annotations from previous verification attempts, and then applies them for verifying new programs. We present a case study where we applied our algorithm to Microsoft’s Static Driver Verifier (SDV). SDV is an industrial-strength tool for verification of Windows device drivers that uses manually-tuned heuristics for obtaining a set of annotations. Our technique inferred program annotations comparable in performance to the existing annotations used in SDV that were devised manually by human experts over years. Additionally, the inferred annotations together with the existing ones improved the performance of SDV overall, proving correct 47% of drivers more while running 22% faster in our experiments.
- A. Albarghouthi, A. Gurfinkel, Y. Li, S. Chaki, and M. Chechik. Ufo: Verification with interpolants and abstract interpretation. In Tools and Algorithms for the Construction and Analysis of Systems, pages 637–640. Springer, 2013. Google ScholarDigital Library
- T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with SLAM. Communications of the ACM, 54(7):68–76, 2011. Google ScholarDigital Library
- T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22, 2001, pages 203–213, 2001. Google ScholarDigital Library
- N. E. Beckman, A. V. Nori, S. K. Rajamani, R. J. Simmons, S. Tetali, and A. V. Thakur. Proofs from tests. IEEE Trans. Software Eng., 36(4):495–508, 2010. Google ScholarDigital Library
- D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, and P. Wendler. Precision reuse for efficient regression verification. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, August 18-26, 2013, pages 389–399, 2013. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238–252, 1977. Google ScholarDigital Library
- A. M. Dan, Y. Meshman, M. T. Vechev, and E. Yahav. Predicate abstraction for relaxed memory models. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, pages 84–104, 2013.Google Scholar
- G. Fedyukovich, A. Gurfinkel, and N. Sharygina. Incremental verification of compiler optimizations. In NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, pages 300–306, 2014. Google ScholarDigital Library
- C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for esc/java. In FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings, pages 500–517, 2001. Google ScholarDigital Library
- P. Garg, C. Löding, P. Madhusudan, and D. Neider. ICE: A robust framework for learning invariants. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 69–87, 2014. Google ScholarDigital Library
- P. Godefroid, S. K. Lahiri, and C. Rubio-González. Statically validating must summaries for incremental compositional dynamic test generation. In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, pages 112–128, 2011. Google ScholarDigital Library
- B. Godlin and O. Strichman. Regression verification: proving the equivalence of similar programs. Softw. Test., Verif. Reliab., 23(3):241–258, 2013.Google ScholarCross Ref
- T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pages 232–244, 2004. Google ScholarDigital Library
- S. K. Lahiri, K. L. McMillan, R. Sharma, and C. Hawblitzel. Differential assertion checking. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, August 18-26, 2013, pages 345–355, 2013. Google ScholarDigital Library
- A. Lal and S. Qadeer. Powering the static driver verifier using corral. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014, pages 202–212, 2014. Google ScholarDigital Library
- A. Lal and S. Qadeer. A program transformation for faster goal-directed search. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, pages 147–154, 2014. Google ScholarDigital Library
- A. Lal and S. Qadeer. DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 280–290, 2015. Google ScholarDigital Library
- A. Lal, S. Qadeer, and S. K. Lahiri. A solver for reachability modulo theories. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, pages 427–443, 2012. Google ScholarDigital Library
- K. R. M. Leino. This is boogie 2. Manuscript KRML, 178:131, 2008. http://https://github.com/boogie-org/boogie.Google Scholar
- K. L. McMillan and A. Rybalchenko. Computing relational fixed points using interpolation. Technical report, Technical report, 2012. available from authors, 2013.Google Scholar
- Microsoft. The Static Driver Verifier. http://msdn.microsoft.com/en-us/library/windows/ hardware/ff552808(v=vs.85).aspx.Google Scholar
- A. Mishne, S. Shoham, and E. Yahav. Typestate-based semantic code search over partial programs. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, pages 997–1016, 2012. Google ScholarDigital Library
- H. Oh, H. Yang, and K. Yi. Learning a strategy for adapting a program analysis via bayesian optimisation. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 572–588, 2015. Google ScholarDigital Library
- V. Raychev, M. T. Vechev, and A. Krause. Predicting program properties from big code. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 111–124, 2015. Google ScholarDigital Library
- V. Raychev, M. T. Vechev, and E. Yahav. Code completion with statistical language models. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, page 44, 2014. Google ScholarDigital Library
- O. Sery, G. Fedyukovich, and N. Sharygina. Incremental upgrade checking by means of interpolation-based function summaries. In Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22-25, 2012, pages 114–121, 2012.Google Scholar
- R. Sharma and A. Aiken. From invariant checking to invariant inference using randomized search. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 88–105, 2014. Google ScholarDigital Library
- R. S. Zvonimir Pavlinovic, Akash Lal. Inferring annotations for device drivers from verification histories. Technical report, Microsoft Research, April 2016.Google Scholar
Index Terms
- Inferring annotations for device drivers from verification histories
Recommendations
An invariant-based approach to the verification of asynchronous parameterized networks
A uniform verification problem for parameterized systems is to determine whether a temporal property is satisfied for every instance of the system which is composed of an arbitrary number of homogeneous processes. To cope with this problem we combine an ...
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified ...
Toward compositional verification of interruptible OS kernels and device drivers
PLDI '16An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified ...
Comments