eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-02
10271
1
19
10.4230/DagSemProc.10271.1
article
10271 Abstracts Collection – Verification over discrete-continuous boundaries
Becker, Bernd
Cardelli, Luca
Hermanns, Holger
Tahar, Sofiene
From 4 July 2010 to 9 July 2010, the Dagstuhl Seminar 10271
``Verification over discrete-continuous boundaries''
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 or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10271/DagSemProc.10271.1/DagSemProc.10271.1.pdf
Formal verification
cyber-physical systems
analog circuits
theorem proving
systems biology
mean-field methods
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-02
10271
1
9
10.4230/DagSemProc.10271.2
article
A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra
Abraham, Erika
Corzilius, Florian
Loup, Ulrich
Sturm, Thomas
There are several methods for the synthesis and analysis of hybrid
systems that require efficient algorithms and tools for satisfiability
checking. For analysis, e.g., bounded model checking describes
counterexamples of a fixed length by logical formulas, whose
satisfiability corresponds to the existence of such a counterexample.
As an example for parameter synthesis, we can state the correctness of
a parameterized system by a logical formula; the solution set of
the formula gives us possible safe instances of the parameters.
For discrete systems, which can be described by propositional logic
formulas, SAT-solvers can be used for the satisfiability checks. For
hybrid systems, having mixed discrete-continuous behavior, SMT-solvers
are needed. SMT-solving extends SAT with theories, and has its main
focus on linear arithmetic, which is sufficient to handle, e.g.,
linear hybrid systems. However, there are only few solvers for
more expressive but still decidable logics like the
first-order theory of the reals with addition and multiplication --
real algebra. Since the synthesis and analysis of non-linear
hybrid systems requires such a powerful logic, we need efficient
SMT-solvers for real algebra. Our goal is to develop such an
SMT-solver for the real algebra, which is both complete and
efficient.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10271/DagSemProc.10271.2/DagSemProc.10271.2.pdf
SMT-solving
Real Algebra
Hybrid Systems
Verification
Synthesis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-02
10271
1
8
10.4230/DagSemProc.10271.3
article
Network-driven Boolean Normal Forms
Brickenstein, Michael
Dreyer, Alexander
We apply the PolyBoRi framework for Groebner bases computations
with Boolean polynomials to bit-valued problems from algebraic
cryptanalysis and formal verification.
First, we proposed zero-suppressed binary decision
diagrams (ZDDs) as a suitable data structure for Boolean polynomials.
Utilizing the advantages of ZDDs we develop new
reduced normal form algorithms for
linear lexicographical lead rewriting systems.
The latter play an important role in modeling bit-valued components of
digital systems.
Next, we reorder the variables in Boolean polynomial rings with respect
to the topology of digital components. This brings computational algebra
to digital circuits and small scale crypto systems in the first place. We
additionally propose an optimized topological ordering, which tends to
keep the intermediate results small. Thus, we successfully applied the
linear lexicographical lead techniques to non-trivial examples from
formal verification of digital systems.
Finally, we evaluate the performance using benchmark examples from
formal verification and cryptanalysis including equivalence checking of a
bit-level formulation of multiplier components. Before we introduced
topological orderings in PolyBoRi, state of the art for the algebraic approach
was a bit-width of 4 for each factor. By combining our techniques we raised
this bound to 16, which is an important step towards real-world applications.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10271/DagSemProc.10271.3/DagSemProc.10271.3.pdf
Groebner
normal forms
Boolean polynomials
cryptanalysis
verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-11-02
10271
1
13
10.4230/DagSemProc.10271.4
article
Towards more Dependable Verification of Mixed-Signal Systems
Schupfer, Florian
Grimm, Christoph
The verification of complex mixed-signal systems is a challenge, especially considering the impact of parameter variations.
Besides the established approaches like Monte-Carlo or Corner-Case simulation, a novel semi-symbolic approach emerged in recent years.
In this approach, parameter variations and tolerances are maintained as symbolic ranges during numerical simulation runs by using affine arithmetic.
Maintaining parameter variations and tolerances in a symbolic way significantly increases verification coverage.
In the following we give a brief introduction and an overview of research on semi-symbolic simulation of both circuits and systems and discuss possible application for system level verification and optimization.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol10271/DagSemProc.10271.4/DagSemProc.10271.4.pdf
Affine Arithmetic
Range based methods
Verification
Semi-symbolic simulation