2015

 nach oben zur Jahresübersicht

• Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
  Counterexamples for Expected Rewards
  2015 Proceedings of the 20th International Symposium on Formal Methods (FM), Springer, Band: 9109, Seiten: 435 - 452
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  The computation of counterexamples for probabilistic systems has gained a lot of attention during the last few years. All of the proposed methods focus on the situation when the probabilities of certain events are too high. In this paper we investigate how counterexamples for properties concerning expected costs (or, equivalently, expected rewards) of events can be computed. We propose methods to extract a minimal subsystem which already leads to costs beyond the allowed bound. Besides these exact methods, we present heuristic approaches based on path search and on best-first search, which are applicable to very large systems when deriving a minimum subsystem becomes infeasible due to the system size. Experiments show that we can compute counterexamples for systems with millions of states.
• Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
  High-level Counterexamples for Probabilistic Automata
  2015 Log Meth Comput Sci (Logical Methods In Computer Science), Band: 11, Nummer: 1:15, Seiten: 1 - 23
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker PRISM. In this paper we describe how a smallest possible subset of the commands can be identified which together make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.

2014

 nach oben zur Jahresübersicht

• Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  Accelerating Parametric Probabilistic Verification
  2014 Int'l Conf. on Quantitative Evaluation of Systems (QEST), Springer-Verlag, Band: 8657, Seite: 404-420
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present a novel method for computing reachability probabilities of parametric discrete-time Markov chains whose transition probabilities are fractions of polynomials over a set of parameters. Our algorithm is based on two key ingredients: a graph decomposition into strongly connected subgraphs combined with a novel factorization strategy for polynomials. Experimental evaluations show that these approaches can lead to a speed-up of up to several orders of magnitude in comparison to existing approaches.
• Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer
  Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
  In: International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM), Advanced Lectures
  2014, Springer-Verlag, Seiten: 65 - 121,
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper is an introductory survey of available methods for the computation and representation of probabilistic counterexamples for discrete-time Markov chains and probabilistic automata. In contrast to traditional model checking, probabilistic counterexamples are sets of finite paths with a critical probability mass. Such counterexamples are not obtained as a by-product of model checking, but by dedicated algorithms. We define what probabilistic counterexamples are and present approaches how they can be generated. We discuss methods based on path enumeration, the computation of critical subsystems, and the generation of critical command sets, both, using explicit and symbolic techniques.
• Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
  Fast Debugging of PRISM Models
  2014 Int'l Symp. on Automated Technology for Verfication and Analysis, Springer-Verlag
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In addition to rigorously checking whether a system conforms to a specification, model checking can provide valuable feedback in the form of succinct and understandable counterexamples. In the context of probabilistic systems, path- and subsystem-based counterexamples at the state-space level can be of limited use in debugging. As many probabilistic systems are described in a guarded command language like the one used by the popular model checker Prism, a technique identifying a subset of critical commands has recently been proposed. Based on repeatedly solving MAXSAT~instances, our novel approach to computing a minimal critical command set achieves a speed-up of up to five orders of magnitude over the previously existing technique.
• Ralf Wimmer, Erika Ábrahám
  Maybe or Maybe Not - Contributions to Stochastic Verification
  In: Aspekte der Technischen Informatik: Festschrift zum 60. Geburtstag von Bernd Becker
  2014, Monsenstein und Vannerdat, Rolf Drechsler, Seiten: 119 - 127, Rolf Drechsler,
• Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  Minimal Counterexamples for Linear-Time Probabilistic Verification
  2014 Theor Comput Sci
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Counterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counterexample-guided abstraction refinement. In this paper, we propose the usage of minimal critical subsystems of discrete-time Markov chains and Markov decision processes as counterexamples for violated omega-regular properties. Minimality can thereby be defined in terms of the number of states or transitions. This problem is known to be NP-complete for Markov decision processes. We show how to compute such subsystems using mixed integer linear programming and evaluate the practical applicability in a number of experiments. They show that our method yields substantially smaller counterexample than using existing techniques.
• Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster
  Symbolic Counterexample Generation for Large Discrete-Time Markov Chains
  2014 Sci Comput Program, Band: 91, Nummer: A, Seiten: 90 - 114
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper presents several symbolic counterexample generation algorithms for discrete-time Markov chains (DTMCs) violating a PCTL formula. A counterexample is (a symbolic representation of) a sub-DTMC that is incrementally generated. The crux to this incremental approach is the symbolic generation of paths that belong to the counterexample. We consider two approaches. First, we extend bounded model checking and develop a simple heuristic to generate highly probable paths first. We then complement the SAT-based approach by a fully (multi-terminal) BDD-based technique. All symbolic approaches are implemented, and our experimental results show a substantially better scalability than existing explicit techniques. In particular, our BDD-based approach using a method called fragment search allows for counterexample generation for DTMCs with billions of states (up to 10^{15}).

2013

 nach oben zur Jahresübersicht

• Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker
  A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
  2013 CADE, Springer, Band: 7898, Seiten: 193 - 207
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  A symbiosis of iSAT and CAD combines the advantages of both methods resulting in a fast and complete solver. In particular, the interval box determined by iSAT provides precious extra information to guide the CAD-method search routine: We use the interval box to prune the CAD search space in both phases, the projection and the construction phase, forming a search `tube' rather than a search tree. This proves to be particularly beneficial for a CAD implementation designed to search a satisfying assignment pointedly, as opposed to search and exclude conflicting regions.
• Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Becker, Bernd
  Accelerating Parametric Probabilistic Verification
  arXiv, Band: arXiv:1312.3979, 2013
• Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  High-Level Counterexamples for Probabilistic Automata
  2013 Springer-Verlag, Band: 8054, Seiten: 18 - 33
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  simplified to obtain a well-understandable counterexample.
• Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  High-Level Counterexamples for Probabilistic Automata
  , Band: arxiv:1305.5055, 2013
• Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám
  Stochastic Bounded Model Checking: Bounded Rewards and Compositionality
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 243 - 254
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  cases.

2012

 nach oben zur Jahresübersicht

• Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes
  AVACS Technical Report, Nummer: 88, 2012
• Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
  Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties
  2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Verlag Dr. Kovac, Seiten: 169 - 180
• Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
  Minimal Critical Subsystems for Discrete-Time Markov Models
  2012 Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer-Verlag, Band: 7214, Seiten: 299 - 314
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We propose a new approach to compute counterexamples for violated ω-regular properties of discrete-time Markov chains and Markov decision processes. Whereas most approaches compute a set of system paths as a counterexample, we determine a critical subsystem that already violates the given property. In earlier work we introduced methods to compute such subsystems based on a search for shortest paths. In this paper we use SMT solvers and mixed integer linear programming to determine minimal critical subsystems.
• Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker
  Symbolic Counterexample Generation for Discrete-time Markov Chains
  2012 Int'l Symp. on Formal Aspects of Component Software, Springer-Verlag, Band: 7684, Seiten: 134 - 151
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we investigate the generation of counterexamples for discrete-time Markov chains (DTMCs) and PCTL properties. Whereas most available methods use explicit representations for at least some intermediate results, our aim is to develop fully symbolic algorithms. As in most related work, our counterexample computations are based on path search. We first adapt bounded model checking as a path search algorithm and extend it with a novel SAT-solvingheuristics to prefer paths with higher probabilities. As a second approach, we use symbolic graph algorithms to find counterexamples. Experiments show that our approaches, in contrast to other existing techniques, are applicable to very large systems with millions of states.
• Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  The COMICS Tool - Computing Minimal Counterexamples for DTMCs
  2012 Automated Technology for Verification and Analysis, Springer-Verlag, Band: 7561, Seiten: 349 - 353
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper presents the tool COMICS 1.0, which performs model checking and generates counterexamples for DTMCs. For an input DTMC, COMICS computes an abstract system that carries the model checking information and uses this result to compute a critical subsystem, which induces a counterexample. This abstract subsystem can be refined and concretized hierarchically. The tool comes with a command line version as well as a graphical user interface that allows the user to interactively influence the refinement process of the counterexample.
• Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  The COMICS Tool - Computing Minimal Counterexamples for DTMCs
  , Band: arxiv:1206.0603, 2012

2011

 nach oben zur Jahresübersicht

• Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
  Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking
  2011 IFIP Int'l Conf. on Formal Methods for Open Object-based Distributed Systems, Springer-Verlag, Band: 6722, Seiten: 75 - 89
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Generation of counterexamples is a highly important task in the model checking process. In contrast to, e.\,g., digital circuits where counterexamples typically consist of a single path leading to a critical state of the system, in the probabilistic setting counterexamples may consist of a large number of paths. In order to be able to handle large systems and to use the capabilities of modern SAT-solvers, bounded model checking (BMC) for discrete-time Markov chains was established.\par In this paper we introduce the usage of SMT-solving over linear real arithmetic for the BMC procedure. SMT-solving, extending SAT with theories in this context on the one hand leads to a convenient way to express conditions on the probability of certain paths and on the other hand allows to handle Markov reward models. We use the former to find paths with high probability first. This leads to more compact counterexamples. We report on some experiments, which show promising results.
• Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  Hierarchical Counterexamples for Discrete-Time Markov Chains
  2011 Int'l Symp. on Automated Technology for Verification and Analysis, Springer-Verlag, Band: 6996, Seiten: 443 - 452
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper introduces a novel counterexample generation approach for the verification of discrete-time Markov chains (DTMCs) with two main advantages: (1) We generate abstract counterexamples which can be refined in a hierarchical manner. (2) We aim at minimizing the number of states involved in the counterexamples, and compute a critical subsystem of the DTMC whose paths form a counterexample. Experiments show that with our approach we can reduce the size of counterexamples and the number of computation steps by several orders of magnitude.
• Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  Hierarchical Counterexamples for Discrete-Time Markov Chains
  , Band: AIB-2011-11, 2011
• 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.
• Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
  SMT-based Counterexample Generation for Markov Chains
  2011 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Offis Oldenburg, Band: 14, Seiten: 19 - 28
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Counterexamples are a highly important feature of the model checking process. In contrast to, e.\,g., digital circuits where counterexamples typically consist of a single path leading to a critical state of the system, in the probabilistic setting, counterexamples may consist of a large number of paths. In order to be able to handle large systems and to use the capabilities of modern SAT-solvers, bounded model checking (BMC) for discrete-time Markov chains was established.In this paper we introduce the usage of SMT-solving over the reals for the BMC procedure. SMT-solving, extending SAT with theories, leads in this context on the one hand to a convenient way to express conditions on the probability of certain paths and on the other hand to handle Markov Reward models. The former can be used to find paths with high probability first. This leads to more compact counterexamples.We report on some experiments, which show promising results.

2010

 nach oben zur Jahresübersicht

• Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  DTMC Model Checking by SCC Reduction
  2010 Int'l Conf. on Quantitative Evaluation of Systems, IEEE Computer Society, Seiten: 37 - 46
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Discrete-Time Markov Chains (DTMCs) are a widely-usedformalism to model probabilistic systems. On the one hand, availabletools like \textsc{Prism} or \textsc{Mrmc} offer efficient \emph{modelchecking} algorithms and thus support the verification of DTMCs.However, these algorithms do not provide any diagnostic informationin the form of \emph{counterexamples}, which arehighly important for the correction of erroneous systems. On the otherhand, there exist several approaches to generate counterexamples forDTMCs, but all these approaches require the model checking result forcompleteness.In this paper we introduce a model checking algorithm for DTMCs thatalso supports the generation of counterexamples. Our algorithm,based on the detection and abstraction of strongly connectedcomponents, offers \emph{abstract} counterexamples, which can beinteractively refined by the user.
• Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker
  Exploiting Different Strategies for the Parallelization of an SMT Solver
  2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Fraunhofer Verlag, Seiten: 97 - 106
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we present two different parallelization schemes for the SMT solver iSAT, based on (1) the distribution of work by dividing the search space into disjoint parts and exploring them in parallel, thereby exchanging learnt information, and (2) a portfolio approach, where the entire benchmark instance isexplored in parallel by several copies of the same solver but usingdifferent heuristics to guide the search. We also combine bothapproaches such that solvers examine disjoint parts of the searchspace using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT.

2009

 nach oben zur Jahresübersicht

• Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker
  Picoso - A Parallel Interval Constraint Solver
  2009 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications, CSREA Press, Seiten: 473 - 479
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper describes the parallel interval constraint solver Picoso, which can decide (a subclass of) boolean combinations of linear and non-linear constraints. Picoso follows a master/client model based on message passing, making it suitable for any kind of workstation cluster as well as for multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing the overall search space into disjoint parts. Additionally, to prevent the clients from running into identical conflicts, information about conflicts in form of conflict clauses is exchanged among the clients. Performance measurements, using four clients to solve a number of benchmark problems, show that Picoso yields linear speedup compared to the sequential interval constraint solver iSAT, on which the clients of Picoso are based.

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.

2006

 nach oben zur Jahresübersicht

• Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen
  Memory-aware Bounded Model Checking for Linear Hybrid Systems
  2006 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Fraunhofer IIS/EAS, Seiten: 153 - 162
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bounded Model Checking (BMC) is a successful method for refuting properties of erroneous systems. Initially applied to discrete systems only, BMC could be extended to more complex domains like linear hybrid automata. The increasing complexity coming along with these complex models, but alsorecent optimizations of SAT-based BMC, like excessive conflict learning, reveal a memory explosion problem especially for deep counterexamples. In this paper we introduce parametric data types for the internal solverstructure that, taking advantage of the symmetry of BMC problems, remarkably reduce the memory requirements of the solver.
• Erika Ábrahám, Andreas Grüner, Martin Steffen
  Abstract Interface Behavior of Object-Oriented Languages with Monitors
  2006 IFIP Int'l Conf. on Formal Methods for Open Object-based Distributed Systems, Springer-Verlag, Band: 4036, Seiten: 218 - 232
• Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen
  Bounded Model Checking with Parametric Data Structures
  2006 BMC, Band: 174, Nummer: 3, Seiten: 3 - 16
• Erika Ábrahám, Andreas Grüner, Martin Steffen
  Dynamic Heap-Abstraction for Open Object-Oriented Systems with Thread Classes
  , Nummer: TR-0601, 2006
• Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen
  Inductive Proof Outlines for Exceptions in Multithreaded Java
  2006 IPM Int'l Workshop on Foundations of Software Engineering, Band: 159, Seiten: 281 - 279
• 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.

2005

 nach oben zur Jahresübersicht

• Erika Ábrahám, Andreas Grüner, Martin Steffen
  An Open Structural Operational Semantics for an Object-Oriented Calculus with Thread Classes
  , Nummer: TR-0505, 2005
• Erika Ábrahám, Andreas Grüner, Martin Steffen
  Heap-Abstraction for an Object-Oriented Calculus with Thread Classes
  , Nummer: TR-0505, 2005
• Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen
  Optimizing bounded model checking for linear hybrid systems
  2005 Int'l Conf. on Verification, Model Checking and Abstract Interpretation, Springer-Verlag, Band: 3385, Seiten: 396 - 412
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bounded model checking (BMC) is an automatic verification method that is based on finitely unfolding the system's transition relation. BMC has been successfully applied, in particular, for discovering bugs in digital system design. Its success is based on the effectiveness of satisfiability solvers that are used to check for a finite unfolding whether a violating state is reachable. In this paper we improve the BMC approach for linear hybrid systems. Our improvements are tailored to lazy satisfiability solving and follow two complementary directions. First, we optimize the formula representation of the finite unfoldings of the transition relations of linear hybrid systems, and second, we accelerate the satisfiability checks by accumulating and generalizing data that is generated during earlier satisfiability checks. Experimental results show that the presented techniques accelerate the satisfiability checks significantly.

2004

 nach oben zur Jahresübersicht

• Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen
  Optimizing Bounded Model Checking for Linear Hybrid Systems
  , Nummer: 214, 2004
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bounded model checking (BMC) is an automatic verification method that is based on finitely unfolding the system's transition relation. BMC has been successfully applied, in particular, for discovering bugs in digital system design. Its success is based on the effectiveness of satisfiability solvers that are used to check for a finite unfolding whether a violating state is reachable. In this report we improve the BMC approach for linear hybrid systems. Our improvements are tailored to lazy satisfiability solving and follow two complementary directions. First, we optimize the formula representation of the finite unfoldings of the transition relations of linear hybrid systems, and second, we accelerate the satisfiability checks by accumulating and generalizing data that is generated during earlier satisfiability checks. Experimental results show that the presented techniques accelerate the satisfiability checks significantly.