The synergy of precise and fast abstractions for program verification

ABSTRACT

Predicate abstraction is a powerful technique to reduce the state space of a program to a finite and affordable number of states. It produces a conservative over-approximation where concrete states are grouped together according to a given set of predicates. A precise abstraction contains the minimal set of transitions with regards to the predicates, but as a result is computationally expensive. Most model checkers therefore approximate the abstraction to alleviate the computation of the abstract system by trading off precision with cost. However, approximation results in a higher number of refinement iterations, since it can produce more false counterexamples than its precise counterpart. The refinement loop can become prohibitively expensive for large programs.

This paper proposes a new abstraction refinement technique that combines slow and precise predicate abstraction techniques with fast and imprecise ones. It allows computing the abstraction quickly, but keeps it precise enough to avoid too many refinement iterations. We implemented the new algorithm in a state-of-the-art software model checker. Our tests with various real life benchmarks show that the new approach systematically outperforms both precise and imprecise techniques.

REFERENCES

• 1: T. Ball, B. Cook, S. Das, and S. K. Rajamani. Refining Approximations in Software Predicate Abstraction. In TACAS, pages 388--403, 2004.
• 2: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 3: T. Ball, A. Podelski, and S. K. Rajamani. Boolean and Cartesian Abstraction for Model Checking C Programs. STTT, 5(1): 49--58, 2003.
• 4: T. Ball and S. K. Rajamani. Boolean Programs: A Model and Process for Software Analysis. Technical Report 2000-14, Microsoft Research, February 2000.
• 5: T. Ball and S. K. Rajamani. Generating Abstract Explanations of Spurious Counterexamples in C Programs. Technical Report 2002-09, Microsoft Research, September 2002.
• 6: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 7: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 8: Roberto Cavada , Alessandro Cimatti , Anders Franzén , Krishnamani Kalyanasundaram , Marco Roveri , R. K. Shyamasundar, Computing Predicate Abstractions by Integrating BDDs and SMT Solvers, Proceedings of the Formal Methods in Computer Aided Design, p.69-76, November 11-14, 2007 [doi>10.1109/FMCAD.2007.18]
• 9: E. Clarke, M. Talupur, H. Veith, and D. Wang. SAT Based Predicate Abstraction for Hardware Verification. In SAT, 2003.
• 10: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 11: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 12: Edmund M. Clarke , Anubhav Gupta , James H. Kukula , Ofer Shrichman, SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques, Proceedings of the 14th International Conference on Computer Aided Verification, p.265-279, July 27-31, 2002
• 13: Edmund Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav, Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design, v.25 n.2-3, p.105-127, September-November 2004 [doi>10.1023/B:FORM.0000040025.89719.f3]
• 14: Michael Colón , Tomás E. Uribe, Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures, Proceedings of the 10th International Conference on Computer Aided Verification, p.293-304, June 28-July 02, 1998
• 15: Satyaki Das , David L. Dill, Successive Approximation of Abstract Transition Relations, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.51, June 16-19, 2001
• 16: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 17: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 18: A. Gupta and O. Strichman. Abstraction Refinement for Bounded Model Checking. In CAV, pages 112--124, 2005.
• 19: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 20: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 21: Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund Clarke, Word level predicate abstraction and refinement for verifying RTL verilog, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065697]
• 22: Himanshu Jain, Franjo Ivancic, Aarti Gupta, and Malay K. Ganai. Localization and Register Sharing for Predicate Abstraction. In TACAS, pages 397--412, 2005.
• 23: R. Jhala and K. L. McMillan. Interpolant-Based Transition Relation Approximation. In CAV, pages 39--51, 2005.
• 24: R. Jhala and K. L. McMillan. A Practical and Complete Approach to Predicate Refinement. In TACAS, pages 459--473, 2006.
• 25: Kelvin Ku , Thomas E. Hart , Marsha Chechik , David Lie, A buffer overflow benchmark for software model checkers, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321691]
• 26: S. K. Lahiri, T. Ball, and B. Cook. Predicate Abstraction via Symbolic Decision Procedures. Logical Methods in Computer Science, 3(2), 2007.
• 27: S. K. Lahiri, R. Nieuwenhuis, and A. Oliveras. SMT Techniques for Fast Predicate Abstraction. In CAV, LNCS, pages 424--437. Springer, 2006.
• 28: Kenneth L. McMillan. Lazy abstraction with interpolants. In CAV, pages 123--136, 2006.
• 29: Kenneth L. McMillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.250-264, July 27-31, 2002
• 30: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Algorithms, Theory, Verification

Keywords:
CEGAR, abstraction refinement, predicate abstraction