Volume

Dagstuhl Seminar Proceedings, Volume 10271

Publication Details

  • published at: 2010-11-02
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Access Numbers

Documents

No documents found matching your filter selection.
Document
DOI: 10.4230/DagSemProc.10271.1
10271 Abstracts Collection – Verification over discrete-continuous boundaries

Authors: Bernd Becker, Luca Cardelli, Holger Hermanns, and Sofiene Tahar

Abstract
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.
Cite as

Bernd Becker, Luca Cardelli, Holger Hermanns, and Sofiene Tahar. 10271 Abstracts Collection – Verification over discrete-continuous boundaries. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:DagSemProc.10271.1,
  author =	{Becker, Bernd and Cardelli, Luca and Hermanns, Holger and Tahar, Sofiene},
  title =	{{10271 Abstracts Collection – Verification over discrete-continuous boundaries}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.1},
  URN =		{urn:nbn:de:0030-drops-27922},
  doi =		{10.4230/DagSemProc.10271.1},
  annote =	{Keywords: Formal verification, cyber-physical systems, analog circuits, theorem proving, systems biology, mean-field methods}
}
Document
DOI: 10.4230/DagSemProc.10271.2
A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra

Authors: Erika Abraham, Florian Corzilius, Ulrich Loup, and Thomas Sturm

Abstract
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.
Cite as

Erika Abraham, Florian Corzilius, Ulrich Loup, and Thomas Sturm. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{abraham_et_al:DagSemProc.10271.2,
  author =	{Abraham, Erika and Corzilius, Florian and Loup, Ulrich and Sturm, Thomas},
  title =	{{A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.2},
  URN =		{urn:nbn:de:0030-drops-27907},
  doi =		{10.4230/DagSemProc.10271.2},
  annote =	{Keywords: SMT-solving, Real Algebra, Hybrid Systems, Verification, Synthesis}
}
Document
DOI: 10.4230/DagSemProc.10271.3
Network-driven Boolean Normal Forms

Authors: Michael Brickenstein and Alexander Dreyer

Abstract
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.
Cite as

Michael Brickenstein and Alexander Dreyer. Network-driven Boolean Normal Forms. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{brickenstein_et_al:DagSemProc.10271.3,
  author =	{Brickenstein, Michael and Dreyer, Alexander},
  title =	{{Network-driven Boolean Normal Forms}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.3},
  URN =		{urn:nbn:de:0030-drops-27894},
  doi =		{10.4230/DagSemProc.10271.3},
  annote =	{Keywords: Groebner, normal forms, Boolean polynomials, cryptanalysis, verification}
}
Document
DOI: 10.4230/DagSemProc.10271.4
Towards more Dependable Verification of Mixed-Signal Systems

Authors: Florian Schupfer and Christoph Grimm

Abstract
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.
Cite as

Florian Schupfer and Christoph Grimm. Towards more Dependable Verification of Mixed-Signal Systems. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{schupfer_et_al:DagSemProc.10271.4,
  author =	{Schupfer, Florian and Grimm, Christoph},
  title =	{{Towards more Dependable Verification of Mixed-Signal Systems}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.4},
  URN =		{urn:nbn:de:0030-drops-27911},
  doi =		{10.4230/DagSemProc.10271.4},
  annote =	{Keywords: Affine Arithmetic, Range based methods, Verification, Semi-symbolic simulation}
}

Filters

  • Authors
  • A
  • Abraham, Erika
  • B
  • Becker, Bernd
  • Brickenstein, Michael
  • C
  • Cardelli, Luca
  • Corzilius, Florian
  • D
  • Dreyer, Alexander
  • G
  • Grimm, Christoph
  • H
  • Hermanns, Holger
  • L
  • Loup, Ulrich
  • S
  • Schupfer, Florian
  • Sturm, Thomas
  • T
  • Tahar, Sofiene

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact