Sciweavers

Share
TACAS
2010
Springer
255views Algorithms» more  TACAS 2010»
8 years 2 months ago
Satisfiability Modulo the Theory of Costs: Foundations and Applications
Abstract. We extend the setting of Satisfiability Modulo Theories (SMT) by introducing a theory of costs C, where it is possible to model and reason about resource consumption and ...
Alessandro Cimatti, Anders Franzén, Alberto...
FORMATS
2010
Springer
8 years 2 months ago
Natural Domain SMT: A Preliminary Assessment
SMT solvers have traditionally been based on the DPLL(T) algorithm, where the driving force behind the procedure is a DPLL search over truth valuations. This traditional framework ...
Scott Cotton
ENTCS
2007
88views more  ENTCS 2007»
8 years 4 months ago
Mothers of Pipelines
We present a method for pipeline verification using SMT solvers. It is based on a non-deterministic “mother pipeline” machine (MOP) that abstracts the instruction set archite...
Sava Krstic, Robert B. Jones, John O'Leary
CORR
2010
Springer
208views Education» more  CORR 2010»
8 years 4 months ago
Bounded Model Checking of Multi-threaded Software using SMT solvers
The transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an ex...
Lucas Cordeiro, Bernd Fischer 0002
CAV
2008
Springer
121views Hardware» more  CAV 2008»
8 years 6 months ago
The Barcelogic SMT Solver
This is the first system description of the Barcelogic SMT solver, which implements all techniques that our group has been developing over the last four years as well as state-of-t...
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras...
ICSE
2010
IEEE-ACM
8 years 6 months ago
SMT-based bounded model checking for multi-threaded software in embedded systems
The transition from single-core to multi-core processors has made multi-threaded software an important subject over the last years in computer-aided verification. Model checkers ...
Lucas Cordeiro
CAV
2007
Springer
212views Hardware» more  CAV 2007»
8 years 8 months ago
A Tutorial on Satisfiability Modulo Theories
Abstract. Solvers for satisfiability modulo theories (SMT) check the satisfiability of first-order formulas containing operations from various theories such as the Booleans, bit-ve...
Leonardo Mendonça de Moura, Bruno Dutertre,...
CAV
2009
Springer
123views Hardware» more  CAV 2009»
8 years 8 months ago
On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
We consider the decision problem for quantifier-free formulas whose atoms are linear inequalities interpreted over the reals or rationals. This problem may be decided using satisf...
David Monniaux
FROCOS
2007
Springer
8 years 10 months ago
Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
We offer a transition system representing a high-level but detailed architecture for SMT solvers that combine a propositional SAT engine with solvers for multiple disjoint theorie...
Sava Krstic, Amit Goel
KBSE
2009
IEEE
8 years 11 months ago
SMT-Based Bounded Model Checking for Embedded ANSI-C Software
Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structur...
Lucas Cordeiro, Bernd Fischer, João Marques...
books