2 Search Results for "Schanda, Florian"

Document
DOI: 10.4230/LIPIcs.SAT.2025.4
Bit-Precise Reasoning with Parametric Bit-Vectors

Authors: Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
The SMT-LIB theory of bit-vectors is restricted to bit-vectors of fixed width. However, several important applications can benefit from reasoning about bit-vectors of symbolic widths, i.e., parametric bit-vectors. Recent work has introduced an approach for solving formulas over parametric bit-vectors, via an eager translation to quantified integer arithmetic with uninterpreted functions. The approach was shown to be successful for several applications, including the bit-width independent verification of compiler optimizations, invertibility conditions, and rewrite rules. We extend and improve that approach in several aspects. Theoretically, we improve expressiveness by defining a new theory of parametric bit-vectors that supports more operators and allows reasoning about the bit-widths themselves. Algorithmically, we introduce a lazy algorithm that avoids the use of uninterpreted functions and quantified axioms for them. Empirically, we show a significant improvement by implementing and evaluating our approach, and comparing it experimentally to the previous one.
Cite as

Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit-Precise Reasoning with Parametric Bit-Vectors. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.SAT.2025.4,
  author =	{Berger, Zvika and Zohar, Yoni and Niemetz, Aina and Preiner, Mathias and Reynolds, Andrew and Barrett, Clark and Tinelli, Cesare},
  title =	{{Bit-Precise Reasoning with Parametric Bit-Vectors}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{4:1--4:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.4},
  URN =		{urn:nbn:de:0030-drops-237385},
  doi =		{10.4230/LIPIcs.SAT.2025.4},
  annote =	{Keywords: Satisfiability Modulo Theories, Bit-precise Reasoning, Parametric Bit-vectors}
}
Document
DOI: 10.4230/LIPIcs.ICLP.2012.72
Using Answer Set Programming in the Development of Verified Software

Authors: Florian Schanda and Martin Brain

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

Abstract
Software forms a key component of many modern safety and security critical systems. One approach to achieving the required levels of assurance is to prove that the software is free from bugs and meets its specification. If a proof cannot be constructed it is important to identify the root cause as it may be a flaw in the specification or a bug. Novice users often find this process frustrating and discouraging, and it can be time-consuming for experienced users. The paper describes a commercial application based on Answer Set Programming called Riposte. It generates simple counter-examples for false and unprovable verification conditions (VCs). These help users to understand why problematic VC are false and makes the development of verified software easier and faster.
Cite as

Florian Schanda and Martin Brain. Using Answer Set Programming in the Development of Verified Software. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 72-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{schanda_et_al:LIPIcs.ICLP.2012.72,
  author =	{Schanda, Florian and Brain, Martin},
  title =	{{Using Answer Set Programming in the Development of Verified Software}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{72--85},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.72},
  URN =		{urn:nbn:de:0030-drops-36114},
  doi =		{10.4230/LIPIcs.ICLP.2012.72},
  annote =	{Keywords: Answer Set Programming, verification, SPARK, Ada, contract based verification, safety critical}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2012

  • Refine by Author
  • 1 Barrett, Clark
  • 1 Berger, Zvika
  • 1 Brain, Martin
  • 1 Niemetz, Aina
  • 1 Preiner, Mathias
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Automated reasoning

  • Refine by Keyword
  • 1 Ada
  • 1 Answer Set Programming
  • 1 Bit-precise Reasoning
  • 1 Parametric Bit-vectors
  • 1 SPARK
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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