2018

 nach oben zur Jahresübersicht

• Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker
  Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
  In: Advanced Logic Synthesis
  2018, Springer, André Ignacio Reis and Rolf Drechsler, Seiten: 151 - 168, André Ignacio Reis and Rolf Drechsler, ISBN: 978-3-319-67294-6

2016

 nach oben zur Jahresübersicht

• Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker
  Dependency Schemes for DQBF
  2016 Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, Band: 9710, Seiten: 473 - 489
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Dependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of dependency schemes that were proposed for QBF. It turns out that only some of them are sound for DQBF. For the sound ones, we provide a correctness proof, for the others counterexamples. Experiments show that a significant number of dependencies can either be added to or removed from a formula without changing its truth value, but with significantly increasing the flexibility for modifying the representation.
• Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Skolem Functions for DQBF
  2016 Int'l Symposium on Automated Technology for Verification and Analysis (ATVA) Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer, Band: 9938, Seiten: 395 - 411
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.
• Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Skolem Functions for DQBF (Extended Version)
  , 2016

2015

 nach oben zur Jahresübersicht

• Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker
  Preprocessing for DQBF
  2015 Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, Band: 9340, Seiten: 173 - 190
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  For SAT and QBF formulas many techniques are applied in order to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. It is well known that these preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper we generalize different preprocessing techniques for SAT and QBF problems to dependency quantified Boolean formulas (DQBF) and describe how they need to be adapted to work with a DQBF solver core. We demonstrate their effectiveness both for CNF- and non-CNF-based DQBF algorithms.
• Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker
  Solving DQBF Through Quantifier Elimination
  2015 Conf. on Design, Automation and Test in Europe

2013

 nach oben zur Jahresübersicht

• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Equivalence Checking for Partial Implementations Revisited
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Universität Rostock ITMZ, Seiten: 61 - 70
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we consider the problem of checking whether a partial implementation can (still) be extended to a complete design which is equivalent to a given full specification. In particular, we investigate the relationship between the equivalence checking problem for partial implementations (PEC) and the validity problem for quantified boolean formulae (QBF) with so-called Henkin quantifiers. Our analysis leads us to a sound and complete algorithmic solution to the PEC problem as well as to an exact complexity theoretical classification of the problem.
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Equivalence Checking of Partial Designs using Dependency Quantified Boolean Formulae
  2013 Int'l Conf. on Computer Design, IEEE Computer Society, Seiten: 396 - 403
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC. We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.

2011

 nach oben zur Jahresübersicht

• Christian Miller, Karina Gitina, Bernd Becker
  Bounded Model Checking of Incomplete Real-time Systems Using Quantified SMT Formulas
  2011 Int'l Workshop on Microprocessor Test and Verification, Seiten: 22 - 27
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is bounded model checking (BMC) where the system is iteratively unfolded and transformed into a satisfiability problem. In this paper, we apply BMC to incomplete networks of timed automata, i.e. systems containing so-called black boxes. In this context, we answer the question of unrealizability, that is, is a safety property violated regardless of the implementation of the black boxes. We focus on problems where the error path depends on the behavior of the black boxes such that an encoding using universal quantification is needed. This yields more advanced quantified SMT formulas, which can no longer be solved by conventional SMT solvers. Taking several prevalent communication models into account, we show how to encode the unrealizability problem and present several procedures to solve the resulting quantified SMT formulas efficiently using And-Inverter-Graphs extended by linear constraints over reals. Finally, we give experimental results to show the applicability of our verification methods.

2010

 nach oben zur Jahresübersicht

• Christian Miller, Karina Gitina, Christoph Scholl, Bernd Becker
  Bounded Model Checking of Incomplete Networks of Timed Automata
  2010 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, Band: 11, Seiten: 61 - 66
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Verification of real-time systems - e.g. communication protocols or embedded controllers - is an important task. One method to detect errors is called bounded model checking (BMC). In BMC the system is iteratively unfolded and then transformed into a satisfiability problem. If an appropriate solver finds the k-th instance to be satisfiable a counterexample for a given safety property has been found. In this paper we present a first approach to apply BMC to networks of timed automata (that is a system of several interacting subautomata) where parts of the network are unspecified (so called blackboxes). Here, we would like to answer the question of unrealizability, that is, is there a path of a certain length violating a safety property regardless of the implementation of the blackboxes. We provide solutions to this problem for two timed automata communication models. For the simple synchronization model, a BMC approach based on fixed transitions is introduced resulting in a SAT-Modulo-Theory formula. With respect to the use of bounded integer variables for communication, we prove unrealizability by introducing universal quantification, yielding more advanced quantified SAT-Modulo-Theory formulas.