2007

 back to the year overview

• Bernd Becker, Christian Dax, Jochen Eisinger, Felix Klaedtke
  LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals
  2007 Int'l Conf. on CAV, Springer-Verlag, pages: 312 - 315
• Christian Dax, Jochen Eisinger, Felix Klaedtke
  Mechanizing the Powerset Construction for Restricted Classes of omega-Automata
  2007 Int'l Symp. on Automated Technology for Verification and Analysis, Springer-Verlag, volume: 4762, pages: 223 - 236
• Christian Dax, Jochen Eisinger, Felix Klaedtke
  Mechanizing the Powerset Construction for Restricted Classes of omega-Automata
  , issue: 228, 2007
• Bernd Becker, Jochen Eisinger, Felix Klaedtke
  Parallelization of Decision Procedures for Automatic Structures
  2007 Workshop on Omega-Automata

2006

 back to the year overview

• Jochen Eisinger, Felix Klaedtke
  Don't Care Words with an Application to the Automata-based Approach for Real Addition
  2006 Conf. on Computer Aided Verification, volume: 4144, pages: 67 - 80
  » show abstract« hide abstract
  Abstract

  't cares" for BDDs to word languages as a means to reduce the automata sizes. A general result in this paper shows that the minimal weak deterministic Büchi automaton (WDBA) with respect to a given don't care set with certain restrictions is uniquely determined and can be efficiently constructed. We apply don't cares to mechanize a more effective decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on WDBAs.
• Jochen Eisinger, Felix Klaedtke
  Don't Care Words with an Application to the Automata-based Approach for Real Addition
  , issue: 223, 2006
  » show abstract« hide abstract
  Abstract

  Automata are a useful tool in infinite state model checking,since they can represent infinite sets of integers and reals. However, analogous to BDDs to represent finite sets, an obstacle of an automata-based set representation is the sizes of the automata. In this paper, we generalizethe notion of "don't cares" for BDDs to word languages as a means to reduce the automata sizes. A general result in this paper shows that the minimal weak deterministic Büchi automaton (WDBA) with respect to a given don't care set with certain restrictions is uniquely determined and can be efficiently constructed. We apply don't cares to mechanize amore effective decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on WDBAs.

2005

 back to the year overview

• 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, volume: 3385, pages: 396 - 412
  » show abstract« hide abstract
  Abstract

  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

 back to the year overview

• Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen
  Optimizing Bounded Model Checking for Linear Hybrid Systems
  , issue: 214, 2004
  » show abstract« hide abstract
  Abstract

  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.