Franzen, Per Anders
Franzen, Per Anders
A lazy and layered SMT(BV) solver for hard industrial verification problems
2007-01-01 Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Griggio, Alberto; Z., Hanna; A., Nadel; A., Palti; Sebastiani, Roberto
Computing Predicate Abstractions by Integrating BDDs and SMT Solvers
2007-01-01 R., Cavada; A., Cimatti; Franzen, Per Anders; Krishnamani, Kalyanasundaram; Roveri, Marco; R. K., Shyamasundar
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis
2006-01-01 Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Griggio, Alberto; Sebastiani, Roberto
Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT
2010-01-01 Franzen, Per Anders
Encoding RTL Constructs for MathSAT: a Preliminary Report
2006-01-01 M., Bozzano; Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Z., Hanna; Z., Khasidashvili; A., Palti; Sebastiani, Roberto
The MathSAT 4 SMT Solver
2008-01-01 Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Griggio, Alberto; Sebastiani, Roberto
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT (EUF ÈT)
2006-01-01 Bruttomesso, Roberto; A., Cimatti; Franzen, Per Anders; Griggio, Alberto; A., Santuari; Sebastiani, Roberto