Subscribe

Issue No.09 - Sept. (2013 vol.39)

pp: 1283-1307

Juan P. Galeotti , Universidad de Buenos Aires and CONICET, Argentina

Nicolas Rosner , Universidad de Buenos Aires, Argentina

Carlos G. Lopez Pombo , Universidad de Buenos Aires and CONICET, Argentina

Marcelo F. Frias , Instituto Tecnológico de Buenos Aires and CONICET, Argentina

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2013.15

ABSTRACT

SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the failure is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this paper, we present Translation of Annotated COde (TACO), a prototype tool which implements a novel, general, and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate which, on one hand, reduces the size of the search space by ignoring certain classes of isomorphic models and, on the other hand, allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading to an improvement of the efficiency of the analysis of orders of magnitude, compared to the noninstrumented SAT--based analysis. We show that in some cases our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking, or SMT-solving.

INDEX TERMS

Metals, Java, Cost accounting, Instruments, Analytical models, Contracts, Context, DynAlloy, Static analysis, SAT-based code analysis, Alloy, KodKod

CITATION

Juan P. Galeotti, Nicolas Rosner, Carlos G. Lopez Pombo, Marcelo F. Frias, "TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds",

*IEEE Transactions on Software Engineering*, vol.39, no. 9, pp. 1283-1307, Sept. 2013, doi:10.1109/TSE.2013.15REFERENCES

- [1] A. Andoni, D. Daniliuc, S. Khurshid, and D. Marinov, "Evaluating the 'Small Scope Hypothesis'," http://sdg.csail.mit.edu publications.html , 2013.
- [2] D. Babić and A.J. Hu, "Calysto: Scalable and Precise Extended Static Checking,"
Proc. 30th Int'l Conf. Software Eng., 2008.- [3] M. Barnett, B.E. Chang, R. DeLine, B. Jacobs, and K.R.M. Leino, "Boogie: A Modular Reusable Verifier for Object-Oriented Programs,"
Proc. Fourth Int'l Conf. Formal Methods for Components and Objects, pp. 364-387, 2005.- [4] J. Belt, Robby, and X. Deng, "Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-Based Analyses,"
Proc. Seventh Joint Meeting of the European Software Eng. Conf. and the ACM SIGSOFT Symp. The Foundations of Software Eng., pp. 355-364, 2009.- [5] C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M.C. Rinard, "Using First-Order Theorem Provers in the Jahob Data Structure Verification System,"
Proc. Eighth Int'l Conf. Verification, Model Checking, and Abstract Interpretation, pp. 74-88, 2007.- [6] C. Boyapati, S. Khurshid, and D. Marinov, "Korat: Automated Testing Based on Java Predicates,"
Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 123-133, 2002.- [7] E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies, "VCC: A Practical System for Verifying Concurrent C,"
Proc. 22nd Int'l Conf. Theorem Proving in Higher Order Logics, 2009.- [8] P. Cousot and R. Cousot, "Systematic Design of Program Analysis Frameworks,"
Proc. Sixth ACM SIGACT-SIGPLAN Symp. Principles of Programming Languages, pp. 269-282, 1979.- [9] P. Chalin, J.R. Kiniry, G.T. Leavens, and E. Poll, "Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2,"
Proc. Fourth Int'l Conf. Formal Methods for Components and Objects, pp. 342-363, 2005.- [10] E. Clarke, D. Kroening, and F. Lerda, "A Tool for Checking ANSI-C Programs,"
Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 168-176, 2004.- [11] S. Cook, "The Complexity of Theorem-Proving Procedures,"
Proc. Third Ann. ACM Symp. Theory of Computing, pp. 151-158, 1971.- [12] R.A. deMillo, R.J. Lipton, and F.G. Sayward, "Hints on Test Data Selection: Help for the Practicing Programmer,"
Computer, vol. 11, no. 4, pp. 34-41, Apr. 1978.- [13] X. Deng, Robby, and J. Hatcliff, "Towards a Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs,"
Proc. Fifth IEEE Int'l Conf. Software Eng. and Formal Methods, pp. 273-282, 2007.- [14] G. Dennis, "A Relational Framework for Bounded Program Verification," PhD thesis, MIT Press, Sept. 2009.
- [15] G. Dennis, F. Chang, and D. Jackson, "Modular Verification of Code with SAT,"
Proc. Int'l Symp. Software Testing and Analysis, pp. 109-120, 2006.- [16] L. Mendonça de Moura and N. Bjørner, "Z3: An Efficient SMT Solver,"
Proc. 12th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, 2008.- [17] D. Distefano, P. O'Hearn, and H. Yang, "A Local Shape Analysis Based on Separation Logic,"
Proc. 12th Int'l Symp. Software Testing and Analysis, pp. 287-302, 2006.- [18] D. Distefano and M. Parkinson, "Jstar: Towards Practical Verification for Java,"
Proc. 23rd ACM SIGPLAN Conf. Object-Oriented Programming Systems Languages and Applications, pp. 213-226, 2008.- [19] G. Dennis, K. Yessenov, and D. Jackson, "Bounded Verification of Voting Software,"
Proc. Second Int'l Conf. Verified Software: Theories, Tools, Experiments, Oct. 2008.- [20] J. Dolby, M. Vaziri, and F. Tip, "Finding Bugs Efficiently with a SAT Solver,"
Proc. Sixth Joint Meeting of the European Software Eng. Conf. and the ACM SIGSOFT Symp. The Foundations of Software Eng., pp. 195-204, 2007.- [21] J. Edwards, D. Jackson, E. Torlak, and V. Yeung, "Subtypes for Constraint Decomposition,"
Proc. Int'l Symp. Software Testing and Analysis, July 2004.- [22] C. Flanagan, R. Leino, M. Lillibridge, G. Nelson, J. Saxe, and R. Stata, "Extended Static Checking for Java,"
Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 234-245, 2002.- [23] M.F. Frias, J.P. Galeotti, C.G. Lopez Pombo, and N. Aguirre, "DynAlloy: Upgrading Alloy with Actions,"
Proc. 27th Int'l Conf. Software Eng., pp. 442-450, 2005.- [24] M.F. Frias, C.G. Lopez Pombo, J.P. Galeotti, and N. Aguirre, "Efficient Analysis of DynAlloy Specifications,"
ACM Trans. Software Eng. and Methodology, vol. 17, no. 1, 2007.- [25] J.P. Galeotti and M.F. Frias, "DynAlloy as a Formal Method for the Analysis of Java Programs,"
Proc. IFIP Working Conf. Software Eng. Techniques, 2006.- [26] J.P. Galeotti, N. Rosner, C.G. López Pombo, and M.F. Frias, "Analysis of Invariants for Efficient Bounded Verification,"
Proc. 19th Int'l Symp. Software Testing and Analysis, pp. 25-36, 2010.- [27] R. Iosif, "Symmetry Reduction Criteria for Software Model Checking,"
Proc. Ninth Int'l SPIN Workshop Model Checking of Software, pp. 22-41, 2002.- [28] F. Ivančić, Z. Yang, M.K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar, "F-Soft: Software Verification Platform,"
Proc. 17th Int'l Conf. Computer Aided Verification, pp. 301-306, 2005.- [29] D. Jackson,
Software Abstractions. MIT Press, 2006.- [30] D. Jackson and M. Vaziri, "Finding Bugs with a Constraint Solver,"
Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 14-25, 2000.- [31] S. Khurshid, "Generating Structurally Complex Tests from Declarative Constraints," PhD thesis, MIT, http://sdg.csail.mit. edu/pubs/theseskhurshid.phd.pdf , Feb. 2003.
- [32] S. Khurshid, D. Marinov, and D. Jackson, "An Analyzable Annotation Language,"
Proc. 17th ACM SIGPLAN Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 231-245, 2002.- [33] S. Khurshid, D. Marinov, I. Shlyakhter, and D. Jackson, "A Case for Efficient Solution Enumeration,"
Proc. Sixth Int'l Conf. Theory and Applications of Satisfiability Testing, pp. 272-286, 2003.- [34] S. Khurshid and D. Marinov, "TestEra: Specification-Based Testing of Java Programs Using SAT,"
Automated Software Eng. J., vol. 11, no. 4, pp. 403-434, 2004.- [35] K.R.M. Leino, "Specification and Verification of Object-Oriented Software," Marktoberdorf Int'l Summer School, 2008.
- [36] D. Harel, D. Kozen, and J. Tiuryn,
Dynamic Logic. Foundations of Computing. MIT Press, 2000.- [37] Y.-S. Ma, J. Offutt, and Y.-R. Kwon, "MuJava: An Automated Class Mutation System,"
J. Software Testing, Verification, and Reliability, vol. 15, no. 2, pp. 97-133, 2005.- [38] M. Musuvathi and D.L. Dill, "An Incremental Heap Canonicalization Algorithm,"
Proc. 12th Int'l Conf. Model Checking Software, pp. 28-42, 2005.- [39] A. Milicevic, D. Rayside, K. Yessenov, and D. Jackson, "Unifying Execution of Imperative and Declarative Code,"
Proc. 33rd Int'l Conf. Software Eng., May 2011.- [40] R. Rugina and M.C. Rinard, "Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions,"
Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 182-195, 2000.- [41] J.H. Siddiqui and S. Khurshid, "An Empirical Study of Structural Constraint Solving Techniques,"
Proc. 11th Int'l Conf. Formal Eng. Methods: Formal Methods and Software Eng., pp. 88-106, 2009.- [42] E. Torlak and D. Jackson, "Kodkod: A Relational Model Finder,"
Proc. 13th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 632-647, 2007.- [43] M. Vaziri and D. Jackson, "Checking Properties of Heap-Manipulating Procedures with a Constraint Solver,"
Proc. Ninth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 505-520, 2003.- [44] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, "Model Checking Programs,"
Automated Software Eng., vol. 10, no. 2, pp. 203-232, 2003.- [45] W. Visser, C.S. Păsăreanu, and R. Pelánek, "Test Input Generation for Java Containers Using State Matching,"
Proc. Int'l Symp. Software Testing and Analysis, pp. 37-48, 2006.- [46] W. Visser, private communication, second, Feb. 2010.
- [47] Y. Xie and A. Aiken, "Saturn: A Scalable Framework for Error Detection Using Boolean Satisfiability,"
ACM Trans. Programming Languages and Systems, vol. 29, no. 3, 2007. |