eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-17
9461
1
15
10.4230/DagSemProc.09461.1
article
09461 Abstracts Collection – Algorithms and Applications for Next Generation SAT Solvers
Becker, Bernd
Bertacco, Valeria
Drechsler, Rolf
Fujita, Masahiro
From 8th to 13th November 2009, the Dagstuhl Seminar 09461 "Algorithms and Applications for Next Generation SAT Solvers" was held in Schloss Dagstuhl--Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts, slides or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09461/DagSemProc.09461.1/DagSemProc.09461.1.pdf
Boolean Satisfiability
Formal Methods
Word Level
Quantification
Multithreading
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-17
9461
1
2
10.4230/DagSemProc.09461.2
article
Formal Verification of Abstract SystemC Models
Grosse, Daniel
Le, Hoang M.
Drechsler, Rolf
In this paper we present a formal verification approach for abstract SystemC models. The approach allows checking expressive properties and lifts induction known from bounded model checking to a higher level, to cope with the large state space of abstract SystemC programs. The technique is tightly integrated with our SystemC to C transformation and generation of monitoring logic to form a complete and efficient method. Properties specifying both hardware and software aspects, e.g. pre- and post-conditions as well as temporal relations of transactions and events, can be specified. As shown by experiments modern proof techniques allow verifying important non-trivial behavior. Moreover, our inductive technique gives significant speed-ups in comparison to simple methods.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09461/DagSemProc.09461.2/DagSemProc.09461.2.pdf
SystemC
TLM
BMC
SAT
SMT
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-17
9461
1
7
10.4230/DagSemProc.09461.3
article
SMT-Solving for the First-Order Theory of the Reals
Abraham, Erika
Loup, Ulrich
SAT-solving is a highly actual research area with increasing success and plenty of industrial applications. SMT-solving, extending SAT with theories, has its main focus on linear real constrains. However, there are only few solvers going further to more expressive but still decidable logics like the first-order theory of the reals with addition and multiplication.
The main requests on theory solvers that must be fulfilled for their efficient embedding into an SMT solver are (a) incrementality, (b) the efficient computation of minimal infeasible subsets, and (c) the support of backtracking. For the first-order
theory of the reals we are not aware of any solver offering those functionalities.
In this work we address the possibilities to extend existing theory solving algorithms to come up with a theory solver suited for SMT.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09461/DagSemProc.09461.3/DagSemProc.09461.3.pdf
SMT-solving
first-order theory of the reals
verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-17
9461
1
20
10.4230/DagSemProc.09461.4
article
Solving hard instances in QF-BV combining Boolean reasoning with computer algebra
Wedler, Markus
Pavlenko, Evgeny
Dreyer, Alexander
Seelisch, Frank
Stoffel, Dominik
Greuel, Gert-Martin
Kunz, Wolfgang
This paper describes our new satisfyability (SAT) modulo
theory (SMT) solver STABLE for the quantifier-free logic over fixed size
bit vectors. Our main application domain is formal verification
of system-on-chip (SoC) modules designed for complex computational
tasks, for example, in signal processing applications. Ensuring proper
functional behavior for such modules, including arithmetic correctness
of the data paths, is considered a very difficult problem.
We show how methods from computer algebra can be integrated into
an SMT solver such that instances can be handled where the arithmetic
problem parts are specified mixing various levels of abstraction from the
plain gate level for small highly optimized components up to the pure
word level used in high-level specifications. If the arithmetic problem
parts include multiplications such mixed problem descriptions quickly
drive current SMT solvers towards their capacity limits.
High performance data paths are often designed at a level of abstraction
that we call the arithmetic bit level (ABL). We show how ABL information,
if available in an SMT instance, can be used to transform the
decision problem into an equivalent set of variety subset problems. These
problems can be solved efficiently with techniques from computer algebra
based on Gröbner basis theory over finite rings Z/2^n . Sometimes, instances
contain problem parts at a level below the ABL using gate-level
operations. These problem parts, e.g., originate from custom-designed
arithmetic components that are highly optimized using the gate-level
constructs of a hardware description language (HDL). For such cases we
integrate a local ABL extraction technique based on local Reed-Muller
forms.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09461/DagSemProc.09461.4/DagSemProc.09461.4.pdf
SAT modulo Theory
Quantifier Free logic over fixed sized bitvectors; Computer Algebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-17
9461
1
2
10.4230/DagSemProc.09461.5
article
SWORD – Module-based SAT Solving
Wille, Robert
Jung, Jean Christoph
Sülflow, Andre
Drechsler, Rolf
In the paper, SWORD is described – a decision procedure for bit-vector logic that uses SAT techniques and exploits word level information. The main idea of SWORD is based on the following observation: While current SAT solvers perform very well on instances with a large number of logic operations, their performance on arithmetic operations degrades with increasing data-path width. In contrast, pure word-level approaches are able to handle arithmetic operations very fast, but suffer from irregularities in the word-level structure (e.g. bit slicing). SWORD tries to combine the best of both worlds: On the one hand, it includes fast propagation, sophisticated data structures, as well as advanced techniques like non-chronological backtracking and learning from modern SAT solvers. On the other hand word-level information is exploited in the decision heuristic and during propagation.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09461/DagSemProc.09461.5/DagSemProc.09461.5.pdf
SAT Solver
Word Level
SAT Modulo Theories
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-17
9461
1
11
10.4230/DagSemProc.09461.6
article
Towards Model Validation and Verification with SAT Techniques
Gogolla, Martin
After sketching how system development and the UML (Unified Modeling
Language) and the OCL (Object Constraint Language) are related,
validation and verification with the tool USE (UML-based Specification
Environment) is demonstrated. As a more efficient alternative for
verification tasks, two approaches using SAT-based techniques are put
forward: First, a direct encoding of UML and OCL with Boolean
variables and propositional formulas, and second, an encoding
employing an intermediate, higher-level language (KODKOD, stongly
connected to ALLOY). A number of further, presently not realized
verification and validation tasks and the transformation of
higher-level modeling concepts into simple UML/OCL models, which are
checkable with SAT-based techniques, are shortly discussed. Finally,
the potential of SAT-based techniques for model development is again
emphasized.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09461/DagSemProc.09461.6/DagSemProc.09461.6.pdf
UML
OCL
Invariant
Pre- and postcondition
Model validation
Model verification