2017

 nach oben zur Jahresübersicht

• Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris Wirtz
  Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization
  Sci Comput Program, Nummer: 148, Seiten: 123 - 160, 2017

2016

 nach oben zur Jahresübersicht

• Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris Wirtz
  Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization
  SFB/TR 14 AVACS Technical Report, Nummer: 103, 2016

2014

 nach oben zur Jahresübersicht

• Christoph Scholl, Florian Pigorsch, Stefan Disch, Ernst Althaus
  Simple Interpolants for Linear Arithmetic
  2014 DATE, EDA Consortium San Jose, CA, USA / ACM DL

2012

 nach oben zur Jahresübersicht

• Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
  Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
  2012 Sci. Comput. Program., Band: 77, Nummer: 10-11, Seiten: 1122 - 1150

2011

 nach oben zur Jahresübersicht

• Werner Damm, Stefan Disch, Willem Hagemann, Christoph Scholl, Uwe Waldmann, Boris Wirtz
  Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems
  SFB/TR 14 AVACS Technical Report, Nummer: 76, 2011

2009

 nach oben zur Jahresübersicht

• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
  Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
  2009 TACAS, Springer, Band: 5505, Seiten: 383 - 397

2008

 nach oben zur Jahresübersicht

• Christoph Scholl, Stefan Disch
  Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Freiburg, Germany, March 3-5, 2008
  2008 Shaker
• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
  Using an SMT Solver and Craig Interpolation to Detect and Remove Redundant Linear Constraints in Representations of Non-convex Polyhedra
  2008 New York, NY, USA Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, ACM, Seiten: 18 - 26

2007

 nach oben zur Jahresübersicht

• Stefan Disch, Christoph Scholl
  Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets
  2007 ASP Design Automation Conf.
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Combinational equivalence checking is an essential task in circuit design. In this paper we focus on SAT based equivalence checking making use of incremental SAT techniques which are well known from the application inBounded Model Checking. Based on an analysis of shared circuit structures we present heuristics which try to maximize the benefit from incremental SAT solving in this application by looking for good orders in which the equivalence of different circuit outputs is checked. Moreover, we present a reset strategy for situations where the benefit from the incremental SAT approach seems to decrease. Experimental results prove that our novel method outperforms traditional methods significantly.
• Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
  Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
  2007 Berlin / Heidelberg Automated Technology for Verification and Analysis, Springer, Band: 4762, Seiten: 425 - 440
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  (SFB/TR 14 AVACS, http://www.avacs.org/).

2006

 nach oben zur Jahresübersicht

• Florian Pigorsch, Christoph Scholl, Stefan Disch
  Advanced Unbounded CTL Model Checking By Using AIGs, BDD Sweeping, And Quantifier Scheduling
  2006 GI/ITG/GMM Workshop“Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we present a complete method for verifying properties expressed in the temporal logic CTL. In contrast to the majority of verification methods presented in recent years, we support unbounded model checking based on symbolic representations of characteristic functions. Among others, our method is based on an advanced And-Inverter Graph (AIG) implementation, quantifier scheduling, and BDD sweeping. For several examples, our method outperforms BDD based symbolic model checking by orders of magnitude. However, our approach is also able to produce competitive results for cases where BDD are known to perform well.
• Florian Pigorsch, Christoph Scholl, Stefan Disch
  Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling
  2006 Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD), IEEE Computer Society Press, Seiten: 89 - 96
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we present a complete method for verifying properties expressed in the temporal logic CTL. In contrast to the majority of verification methods presented in recent years, we support unbounded model checking based on symbolic representations of characteristic functions. Among others, our method is based on an advanced And-Inverter Graph (AIG) implementation, quantifier scheduling, and BDD sweeping. For several examples, our method outperforms BDD based symbolic model checking by orders of magnitude. However, our approach is also able to produce competitive results for cases where BDD are known to perform well.
• Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
  Automatic verification of hybrid systems with large discrete state space
  2006 Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, Springer-Verlag, Band: 4218
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We address the problem of model checking hybrid systems which exhibit nontrivial discrete behavior and thus cannot be treated by considering the discrete states one by one, as most currently available verification tools do. Our procedure relies on a deep integration of several techniques and tools. An extension of And-Inverter-Graphs (AIGs) with first-order constraints serves as a compact representation format for sets of configurations which are composed of continuous regions and discrete states. Boolean reasoning on the AIGs is complemented by first-order reasoning in various forms and on various levels. These include implication checks for simple constraints, test vector generation for fast inequality checks of boolean combinations of constraints, and an exact subsumption check for representations of two configurations. These techniques are integrated within a model checker for universal CTL. Technically, it deals with discrete-time hybrid systems with linear differentials. The paper presents the approach, its prototype implementation, and first experimental data.