Ergebnisse der Suche:
- [Scheibler et al.,
2016]
- Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin
Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, and Bernd
Becker.
Extending iSAT3 with ICP-contractors for bitwise integer operations.
AVACS Technical Report No. 116, SFB/TR 14 AVACS, 2016.
ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close) Up to now SMT-solvers addressing
floating-point arithmetic were based on bit-blasting. Quite recently, methods
based on interval constraint propagation (ICP) for accurate reasoning over
floating-point arithmetic were proposed. One prominent use-case for such
methods is automatic dead-code detection in floating-point dominated embedded
C programs. However, C programs usually contain a mix of floating-point
arithmetic, integer arithmetic and bitwise integer operations. Thus, adding
ICP-based support for floating-point arithmetic is not enough -- bitwise
integer operations have to be supported as well. Therefore, this report gives
a detailed overview how these operations can be handled with
ICP.
Subproject(s): T1
|
|  Bibtex
|  PDF open |
- [Dinh et al.,
2011]
- Nam Thang Dinh, Martin Fränzle, and Andreas Eggers.
AVACS H1/2 8-year benchmark: Analyzing traffic models with iSAT.
AVACS Technical Report No. 81, SFB/TR 14 AVACS, July 2011.
ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close) In this technical report, we present
an application of the iSAT constraint solver to instances of traffic flow
networks.We give an account of the underlying model and provide details of
different instances of the model and a variety of verification and
falsification tasks handled by our
solver.
Subproject(s):
H1/2
|
|  Bibtex
|  PDF open |
- [Teige and Fränzle,
2011a]
- Tino Teige and Martin Fränzle.
Generalized Craig interpolation for stochastic Boolean satisfiability
problems.
AVACS Technical Report No. 67, SFB/TR 14 AVACS, 2011.
ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close) The stochastic Boolean satisfiability
(SSAT) problem has been introduced by Papadimitriou in 1985 when adding a
probabilistic model of uncertainty to propositional satisfiability through
randomized quantification. SSAT has many applications, among them bounded
model checking (BMC) of symbolically represented Markov decision processes.
This paper identifies a notion of Craig interpolant for the SSAT
framework and develops an algorithm for computing such interpolants based on
SSAT resolution. As a potential application, we address the use of
interpolation in SSAT-based BMC, turning the falsification procedure into a
verification approach for probabilistic safety
properties.
Subproject(s):
H1/2,H4
|
|  Bibtex
|  PDF open |
- [Eggers et al.,
2008b]
- Andreas Eggers, Martin Fränzle, and Christian Herde.
SAT modulo ODE: A direct SAT approach to hybrid systems.
AVACS Technical Report No. 37, Sonderforschungsbereiche (SFB)/ Transregio (TR)
14 AVACS, April 2008.
ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close) In order to facilitate automated
reasoning about large Boolean combinations of non-linear arithmetic
constraints involving ordinary differential equations (ODEs), we provide a
seamless integration of safe numeric overapproximation of initial-value
problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic
constraint solving. Interval-based safe numeric approximation of ODEs is used
as an interval contractor being able to narrow candidate sets in phase space
in both temporal directions: post-images of ODEs (i.e., sets of states
reachable from a set of initial values) are narrowed based on partial
information about the initial values and, vice versa, pre-images are narrowed
based on partial knowledge about post-sets. In contrast to the related CLP(F)
approach of Hickey and Wittenberg, we do (a) support coordinate
transformations mitigating the wrapping effect encountered upon iterating
interval-based overapproximations of reachable state sets and (b) embed the
approach into an SMT framework, thus accelerating the solving process through
the algorithmic enhacements of recent SAT solving
technology.
Subproject(s):
H1/2
|
|  Bibtex
|  PDF open |
- [Kupferschmid et al.,
2008c]
- Stefan Kupferschmid, Tino Teige, Bernd Becker, and
Martin Fränzle.
Proofs of unsatisfiability for mixed boolean and non-linear arithmetic
constraint formulae.
AVACS Technical Report No. 40, Sonderforschungsbereiche (SFB)/ Transregio (TR)
14 AVACS, June 2008.
ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close) In recent years, the use of
constraint solvers for analysis and verification of industrial systems has
become increasingly popular. The correctness and reliability of the results
returned by the employed solvers are a vital requirement, in particular for
safety-critical systems. If a solver proves the satisfiability of a
constraint system and returns a solution then the answer of the solver can be
validated by means of the solution. However, in case the solver claims that
the constraint system is unsatisfiable without any certificate then the
validation of this answer is not that simple. In this paper, we establish the
theoretical basis of generating proofs of unsatisfiability in the mixed
Boolean and non-linear arithmetic constraint framework over the reals and
integers. To do so, we propose a simple rule-based calculus for unsatisfiable
mixed Boolean-arithmetic constraints to produce and check unsatisfiability
proofs. Furthermore, we enhance the iSAT constraint solver to generate
unsatisfiability proofs, we implement a tool validating such proofs, and give
some experimental results.
Subproject(s):
H1/2
|
|  Bibtex
|  PDF open |
- [Teige et al., 2008]
- Tino
Teige, Christian Herde, Martin Fränzle, and Erika Ábrahám.
Conflict analysis and restarts in a mixed boolean and non-linear arithmetic
constraint solver.
AVACS Technical Report No. 34, Sonderforschungsbereiche (SFB)/ Transregio (TR)
14 AVACS, January 2008.
ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close) The recently presented constraint
solver HySAT tackles the in general undecidable problem of solving mixed
Boolean and non-linear arithmetic constraint formulae over the reals
involving transcendental functions. The algorithmic core of HySAT is the iSAT
algorithm, a tight integration of the Davis-Putnam-Logemann-Loveland
algorithm with interval constraint propagation enriched by enhancements like
conflict-driven clause learning and non-chronological backtracking. However,
it was an open question whether HySAT's conflict analysis scheme, an adapted
first unique implication point technique as applied in most modern SAT
solvers, performs favorably compared to other schemes. In this paper, we
compare several conflict analysis heuristics to answer this question.
Furthermore, we consider the integration of restarts into the iSAT algorithm
and investigate their impact. For our empirical results we use benchmarks
from the hybrid systems domain.
Subproject(s):
H1/2
|
|  Bibtex
|  PDF open |
- [Fränzle et al.,
2007b]
- Martin Fränzle, Hardi Hungar, Christian Schmitt, and
Boris Wirtz.
Hlang: Compositional representation of hybrid systems via predicates.
AVACS Technical Report No. 20, SFB/TR 14 AVACS, July 2007.
ISSN: 1860-9821, http://www.avacs.org.
Abstract (click to open/close) Given the structural diversity of
modeling paradigms for hybridsystems that are in widespread use, which ranges
from asignal-transducer-based view like in Simulink/Stateflow to
anautomaton-based view in various hybrid automata frameworks, there isneed
for an intermediate-level language that can accommodate thesestructures in a
concise way, thereby isolating verification backendsfrom the particular
modeling frontend used.This technical report provides a description of the
intermediate-levelmodeling language for hybrid systems used in project area H
of AVACS asa gateway to verification
backends.
Subproject(s):
H1/2,H3
|
|  Bibtex
|  PDF open |
|