2008

 back to the year overview

• Jochen Eisinger
  Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic
  2008 EACSL Annual Conf. on Computer Science Logic, Springer-Verlag, pages: 430 - 444

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

• Jan Reineke, Björn Wachter, Stephan Thesing, Reinhard Wilhelm, Jochen Eisinger, Ilia Polian, Bernd Becker
  A Definition and Classification of Timing Anomalies
  2006 Int'l Workshop on Worst-Case Execution Time
• Jochen Eisinger, Ilia Polian, Bernd Becker, Alexander Metzner, Stephan Thesing, Reinhard Wilhelm
  Automatic Identification of Timing Anomalies for Cycle-Accurate Worst-Case Execution Time Analysis
  2006 IEEE Design and Diagnostics of Electronic Circuits and Systems, IEEE Computer Society, pages: 15 - 20
• 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

• Jochen Eisinger, Peter Winterer, Bernd Becker
  Securing Wireless Networks in a University Environment
  2005 IEEE Int'l Conf. on Pervasive Computing and Communications Workshops, IEEE Computer Society, pages: 312 - 316