Dagstuhl Seminar Proceedings, Volume 10271
Dagstuhl Seminar Proceedings
DagSemProc
https://www.dagstuhl.de/dagpub/1862-4405
https://dblp.org/db/series/dagstuhl
1862-4405
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
10271
2010
https://drops.dagstuhl.de/entities/volume/DagSemProc-volume-10271
10271 Abstracts Collection – Verification over discrete-continuous boundaries
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.
Formal verification
cyber-physical systems
analog circuits
theorem proving
systems biology
mean-field methods
1-19
Regular Paper
Bernd
Becker
Bernd Becker
Luca
Cardelli
Luca Cardelli
Holger
Hermanns
Holger Hermanns
Sofiene
Tahar
Sofiene Tahar
10.4230/DagSemProc.10271.1
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra
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.
SMT-solving
Real Algebra
Hybrid Systems
Verification
Synthesis
1-9
Regular Paper
Erika
Abraham
Erika Abraham
Florian
Corzilius
Florian Corzilius
Ulrich
Loup
Ulrich Loup
Thomas
Sturm
Thomas Sturm
10.4230/DagSemProc.10271.2
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Network-driven Boolean Normal Forms
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.
Groebner
normal forms
Boolean polynomials
cryptanalysis
verification
1-8
Regular Paper
Michael
Brickenstein
Michael Brickenstein
Alexander
Dreyer
Alexander Dreyer
10.4230/DagSemProc.10271.3
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Towards more Dependable Verification of Mixed-Signal Systems
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.
Affine Arithmetic
Range based methods
Verification
Semi-symbolic simulation
1-13
Regular Paper
Florian
Schupfer
Florian Schupfer
Christoph
Grimm
Christoph Grimm
10.4230/DagSemProc.10271.4
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode