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 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.

This software is also peer reviewed by journal TOMS.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 7 articles , 1 standard article )

Showing results 1 to 7 of 7.
Sorted by year (citations)

  1. Ponzio, Pablo; Godio, Ariel; Rosner, Nicolás; Arroyo, Marcelo; Aguirre, Nazareno; Frias, Marcelo F.: Efficient bounded model checking of heap-manipulating programs using tight field bounds (2021)
  2. Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
  3. Pham, Long H.; Le, Quang Loc; Phan, Quoc-Sang; Sun, Jun; Qin, Shengchao: Enhancing symbolic execution of heap-based programs with separation logic for test input generation (2019)
  4. Kirches, Christian; Leyffer, Sven: TACO: a toolkit for AMPL control optimization (2013)
  5. Yang, Guowei; Khurshid, Sarfraz; Kim, Miryung: Specification-based test repair using a lightweight formal method (2012) ioport
  6. Aguirre, Nazareno M.; Bengolea, Valeria S.; Frias, Marcelo F.; Galeotti, Juan P.: Incorporating coverage criteria in bounded exhaustive black box test generation of structural inputs (2011) ioport
  7. Cuervo Parrino, Bruno; Galeotti, Juan Pablo; Garbervetsky, Diego; Frias, Marcelo F.: A dataflow analysis to improve SAT-based bounded program verification (2011) ioport