Nicolás Rosner
Juan Galeotti
ABSTRACT
In this article we present a novel technique for automated parallel bug-finding based on the sequential analysis tool TACO. TACO is a tool based on SAT-solving for efficient bug-finding in Java code with rich class invariants. It prunes the SAT-solver's search space by introducing precise symmetry-breaking predicates and bounding the relational semantics of Java class fields. The bounds computed by TACO generally include a substantial amount of nondeterminism; its reduction allows us to split the original analysis into disjoint subproblems. We discuss the soundness and completeness of the decomposition. Furthermore, we present experimental results showing that MUCHO-TACO, our tool which implements this technique, yields significant speed-ups over TACO on commodity cluster hardware.
- Abad P., Aguirre N., Bengolea V., Ciolek D., Frias M.F., Galeotti J., Maibaum T., Moscato M., Rosner N., Vissani I., Tight Bounds + Incremental SAT = Better Test Generation under Rich Contracts, to appear in Proceedings of ICST 2013.Google Scholar
- Belt, J., Robby and Deng X., Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analyses, FSE 2009, pp. 355–364. Google ScholarDigital Library
- Dolby J., Vaziri M., Tip F., Finding Bugs Efficiently with a SAT Solver, in ESEC/FSE’07, pp. 195–204, ACM Press, 2007. Google ScholarDigital Library
- Bouillaguet Ch., Kuncak V., Wies T., Zee K., Rinard M.C., Using First-Order Theorem Provers in the Jahob Data Structure Verification System. VMCAI 2007, pp. 74–88. Google ScholarDigital Library
- Chandrasekhar Boyapati, Sarfraz Khurshid, Darko Marinov: Korat: automated testing based on Java predicates. ISSTA 2002: 123-133. Google ScholarDigital Library
- Chalin P., Kiniry J.R., Leavens G.T., Poll E. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. FMCO 2005: 342-363. Google ScholarDigital Library
- Wahid Chrabakh and Rich Wolski, GrADSAT: A Parallel SAT Solver for the Grid, in UCSB Computer Science Technical Report Number 2003-05.Google Scholar
- Cuervo-Parrino B., Galeotti J.P., Garbervetsky D., Frias M.F., A dataflow analysis to improve SAT-based program verification, to appear in Proceedings of SEFM 2011. Google ScholarDigital Library
- Deng, X., Robby, Hatcliff, J., Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs, in SEFM 2007, pp. 273-282. Google ScholarDigital Library
- Dennis, G., Chang, F., Jackson, D., Modular Verification of Code with SAT. in ISSTA’06, pp. 109–120, 2006. Google ScholarDigital Library
- Flanagan, C., Leino, R., Lillibridge, M., Nelson, G., Saxe, J., Stata, R., Extended static checking for Java, In PLDI 2002, pp. 234–245. Google ScholarDigital Library
- Juan P. Galeotti, Nicolás Rosner, Carlos López Pombo, Marcelo F. Frias: Analysis of invariants for efficient bounded verification. ISSTA 2010: 25–36. Google ScholarDigital Library
- Juan P. Galeotti, Nicolás Rosner, Carlos López Pombo, Marcelo F. Frias: TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds, submitted to IEEE TSE, 2013.Google Scholar
- Lu´ıs Gil, Paulo Flores and Lu´ıs Miguel Silveira: PMSat: a parallel version of MiniSAT, Journal on Satisfiability, Boolean Modeling and Computation 6 (2008) 71-98.Google ScholarCross Ref
- Daniel Jackson, Ian Schechter, and Ilya Shlyakhter. Alcoa: the alloy constraint analyzer. In Proceedings of International Conference on Software Engineering, Limerick, Ireland, 2000. Google ScholarDigital Library
- Jackson, D., Software Abstractions. MIT Press, 2006.Google Scholar
- Jackson, D., Vaziri, M., Finding bugs with a constraint solver, in ISSTA’00, pp. 14-25, 2000. Google ScholarDigital Library
- Khurshid S. and Marinov D., TestEra: Specification-Based Testing of Java Programs Using SAT., Automated Software Engineering 11(4): 403–434 (2004) Google ScholarDigital Library
- Leino K.R.M., Specification and verification of Object-Oriented Software, Lecture Notes from Marktoberdorf International Summer School 2008.Google Scholar
- Kei Ohmura and Kazunori Ueda, c-sat: A Parallel SAT Solver for Clusters, in SAT 2009, LNCS 5585, 2009. Google ScholarDigital Library
- Danhua Shao, Divya Gopinath, Sarfraz Khurshid, Dewayne E. Perry, Optimizing Incremental Scope-Bounded Checking with Data-Flow Analysis. ISSRE 2010: 408–417. Google ScholarDigital Library
- Danhua Shao, Sarfraz Khurshid, Dewayne E. Perry: An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method. FM 2009: 757–772. Google ScholarDigital Library
- Rohan Sharma, Milos Gligoric, Andrea Arcuri, Gordon Fraser, Darko Marinov: Testing Container Classes: Random or Systematic? FASE 2011: 262-277. Google ScholarDigital Library
- Siddiqui J.H., and Khurshid S., PKorat: Parallel Generation of Structurally Complex Test Inputs, in Proceedings of ICST’09. Google ScholarDigital Library
- Matt Staats, Corina S. Pasareanu: Parallel symbolic execution for structural test generation. ISSTA 2010: 183-194 Google ScholarDigital Library
- Torlak E., Jackson, D., Kodkod: A Relational Model Finder. in TACAS ’07, LNCS 4425, pp. 632–647. Google ScholarDigital Library
- Vaziri, M., Jackson, D., Checking Properties of Heap-Manipulating Procedures with a Constraint Solver, in TACAS 2003, pp. 505-520. Google ScholarDigital Library
- Visser W., Havelund K., Brat G., Park S. and Lerda F., Model Checking Programs, ASE Journal, Vol.10, N.2, 2003. Google ScholarDigital Library
- Visser W., Păsăreanu C. S., Pelánek R., Test Input Generation for Java Containers using State Matching, in ISSTA 2006, pp. 37–48, 2006. Google ScholarDigital Library
- Hantao Zhang, Maria Paola Bonacina, and Jieh Hsiang. 1996. PSATO: a distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21, 4-6 (June 1996). Google ScholarDigital Library
Index Terms
- Parallel bounded analysis in code with rich invariants by refinement of field bounds
Recommendations
Analysis of invariants for efficient bounded verification
ISSTA '10: Proceedings of the 19th international symposium on Software testing and analysisSAT-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 ...
TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds
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 ...
Static program analysis of embedded executable assembly code
CASES '04: Proceedings of the 2004 international conference on Compilers, architecture, and synthesis for embedded systemsWe consider the problem of automatically checking if coding standards have been followed in the development of embedded applications. The problem arises from practical considerations because DSP chip manufacturers (in our case Texas Instruments) want ...
Comments