Abstract
Precise software analysis and verification require tracking the exact path along which a statement is executed (path-sensitivity), the different contexts from which a function is called (context-sensitivity), and the bit-accurate operations performed. Previously, verification with such precision has been considered too inefficient to scale to large software. In this paper, we present a novel approach to solving such verification conditions, based on an automatic abstraction-checking-refinement framework that exploits natural abstraction boundaries present in software. Experimental results show that our approach easily scales to over 200,000 lines of real C/C++ code.
Research supported by a Microsoft Graduate Fellowship and an NSERC Discovery Grant.
Chapter PDF
References
Babić, D., Hu, A.: Fast Symbolic Execution for Static Checking (submitted for publication)
Babić, D., Musuvathi, M.: Modular Arithmetic Decision Procedure. Technical Report TR-2005-114, Microsoft Research Redmond (2005)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic Predicate Abstraction of C Programs. Programming Language Design and Implementation, pp. 203–213 (2001)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. Programming Language Design and Implementation, pp. 196–207 (2003)
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Design Automation Conference, pp. 368–371 (2003)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Trans Programming Languages and Systems 13(4), 451–490 (1991)
Dijkstra, E.W., Scholten, C.S. (eds.): Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)
Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. Programming Language Design and Implementation, pp. 234–245 (2002)
Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. Principles of Programming Languages, pp. 193–205 (2001)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. Principles of Programming Languages, pp. 58–70 (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. Principles of Programming Languages, pp. 232–244 (2004)
Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: CGO 2004. Proceedings of the International Symposium on Code Generation and Optimization, p. 75. IEEE Computer Society, Washington, DC, USA (2004)
Leino, K.R.M., Müller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 115–130. Springer, Heidelberg (2006)
Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281–288 (2005)
Livshits, V.B., Lam, M.S.: Tracking Pointers with Path and Context Sensitivity for Bug Detection in C Programs. In: European Software Engineering Conference/International Symposium on Foundations of Software Engineering, pp. 317–326 (2003)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. Principles of Programming Languages, pp. 49–61 (1995)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pp. 466–483. Springer, Heidelberg (1983)
Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. Programming Language Design and Implementation, pp. 131–144 (2004)
Wilson, C., Dill, D.L.: Reliable verification using symbolic simulation with scalar values. In: 37th Design Automation Conference, pp. 124–129. ACM/IEEE (2000)
Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. Principles of Programming Languages, pp. 351–363 (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Babić, D., Hu, A.J. (2007). Structural Abstraction of Software Verification Conditions. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_41
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)