2011

 nach oben zur Jahresübersicht

• Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde
  Parallel SAT Solving in Bounded Model Checking
  2011 Journal of Logic and Computation, Band: 21, Nummer: 1, Seiten: 5 - 21
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.

2007

 nach oben zur Jahresübersicht

• Marc Herbstritt, Bernd Becker, Erika Ábrahám, Christian Herde
  On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata
  2007 IEEE Design and Diagnostics of Electronic Circuits and Systems, IEEE Computer Society, Seiten: 391 - 396
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  rithmic structure of the combined SAT-LP-solver, and (2) efficiency issues in form of a counter-based design that adapts the popular concept of the VSIDS heuristics of Chaff. An empirical analysis ofour framework shows (1) the importance of guard variables related to real-valued constraints and (2) reveals an ambiguity between the number of calls of the LP-solver and the time used by the LP-solver. As a result, we propose a simple, but efficient, variable selection heuristics that takes our observations into account and experimentally overcomes the limitations of existing ones.
• Martin Fränzle, Christian Herde, Tino Teige, S. Ratschan, Tobias Schubert
  Efficient Solving of Large Non-Linear Arithmetic Constraint Systems with Complex Boolean Structure
  2007 Journal on Satisfiability, Boolean Modeling, and Computation, Band: 1, Nummer: 3-4, Seiten: 209 - 236

2006

 nach oben zur Jahresübersicht

• Martin Fränzle, Christian Herde, S. Ratschan, Tobias Schubert, Tino Teige
  Interval Constraint Solving Using Propositional SAT Solving Techniques
  2006 Int'l Workshop on the Integration of SAT and CP Techniques, Seiten: 81 - 95
• Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde
  Parallel SAT-Solving in Bounded Model Checking
  2006 Int'l Workshop on Parallel and Distributed Methods in Verification, Springer-Verlag, Band: 4346, Seiten: 301 - 315
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bounded Model Checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver.We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.

2004

 nach oben zur Jahresübersicht

• Bernd Becker, Markus Behle, Friedrich Eisenbrand, Martin Fränzle, Marc Herbstritt, Christian Herde, Jörg Hoffmann, Daniel Kröning, Bernhard Nebel, Ilia Polian, Ralf Wimmer
  Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems
  2004 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Seiten: 65 - 75
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present a concept to significantly advance the state of the art for bounded model checking (BMC) and inductive verification (IV) of hybrid discrete-continuous systems. Our approach combines the expertise of partners coming from different domains, like hybrid systems modeling and digital circuit verification, bounded planning and heuristic search, combinatorial optimization and integer programming. After sketching the overall verification flow we present first results indicating that the combination and tight integration of different verification engines is a first step to pave the way to fully automated BMC and IV of medium to large-scale networks of hybrid automata.