Karina Wimmer, Dipl.-Inf.
Technische Fakultät Albert-Ludwigs-Universität Georges Köhler Allee, Gebäude 51 79110 Freiburg im Breisgau Deutschland
Gebäude 51, Raum 01..030
+49 (0)761 203 8146
+49 (0)761 203 8142
gitina@informatik.uni-freiburg.de
Karina Wimmer
Liste filtern : Jahre: 2016 |
2015 |
2013 |
2011 |
2010 | alle anzeigen nach oben zur Jahresübersicht Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd BeckerDependency 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 BeckerSkolem 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 BeckerSkolem Functions for DQBF (Extended Version) , 2016 nach oben zur Jahresübersicht Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd BeckerPreprocessing 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 BeckerSolving DQBF Through Quantifier Elimination 2015 Conf. on Design, Automation and Test in Europe nach oben zur Jahresübersicht Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd BeckerEquivalence 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 BeckerEquivalence 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 We consider the partial equivalence checking problem (PEC), i.e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied.
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. nach oben zur Jahresübersicht Christian Miller, Karina Gitina, Bernd BeckerBounded 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. nach oben zur Jahresübersicht Christian Miller, Karina Gitina, Christoph Scholl, Bernd BeckerBounded 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.