Search For:

Displaying 1-5 out of 5 total
TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds
Found in: IEEE Transactions on Software Engineering
By Juan P. Galeotti,Nicolas Rosner,Carlos G. Lopez Pombo,Marcelo F. Frias
Issue Date:September 2013
pp. 1283-1307
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 tra...
Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving
Found in: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation (ICST)
By Pablo Abad,Nazareno Aguirre,Valeria Bengolea,Daniel Ciolek,Marcelo F. Frias,Juan Galeotti,Tom Maibaum,Mariano Moscato,Nicolas Rosner,Ignacio Vissani
Issue Date:March 2013
pp. 21-30
We present a novel and general technique for automated test generation that combines tight bounds with incremental SAT solving. The proposed technique uses incremental SAT to build test suites targeting a specific testing criterion, amongst various black-b...
Dynamite: A tool for the verification of alloy models based on PVS
Found in: ACM Transactions on Software Engineering and Methodology (TOSEM)
By Carlos G. Lopez Pombo, Marcelo F. Frias, Mariano M. Moscato
Issue Date:March 2014
pp. 1-37
Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT solvers. The translation requires user-provided bounds on the sizes of dat...
Parallel bounded analysis in code with rich invariants by refinement of field bounds
Found in: Proceedings of the 2013 International Symposium on Software Testing and Analysis (ISSTA 2013)
By Guido Marucci Blas, Juan Galeotti, Lucas Pizzagalli, Luciano Zemín, Marcelo F. Frias, Nicolás Rosner, Santiago Bermúdez, Santiago Perez De Rosso
Issue Date:July 2013
pp. 23-33
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'...
A strategy for efficient verification of relational specifications, based on monotonicity analysis
Found in: Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering (ASE '05)
By Gabriela Steren, Lorena Bourg, Marcelo F. Frias, Rodolfo Gamarra
Issue Date:November 2005
pp. 305-308
We introduce a strategy for the verification of relational specifications based on the analysis of monotonicity of variables within formulas. By comparing with the Alloy Analyzer, we show that for a relevant class of problems this technique drastically out...