2016

 nach oben zur Jahresübersicht

• Christoph Scholl, Florian Pigorsch
  The QBF Solver AIGSolve
  2016 International Workshop on Quantified Boolean Formulas
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Intermediate results are represented symbolically using AIGs. The basic method consists of cofactor-based quantifier elimination which is combined with a multitude of optimization approaches including a SAT- and BDD-based compaction of the representations, methods for preprocessing QBF-formulas based on incremental SAT, heuristics that exchange quantifiers of the same level, heuristics that use BDD-based quantifier elimination as an alternative, as well as structure extraction and structure exploitation for the processed instances.

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

2013

 nach oben zur Jahresübersicht

• Florian Pigorsch, Christoph Scholl
  Lemma localization: a practical method for downsizing SMT-interpolants
  2013 DATE, EDA Consortium San Jose, CA, USA / ACM DL, Seiten: 1405 - 1410

2012

 nach oben zur Jahresübersicht

• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
  Enhanced Integration of QBF Solving Techniques
  2012 MBMV, Seiten: 133 - 143
• 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

• Georges Morbé, Florian Pigorsch, Christoph Scholl
  Fully Symbolic Model Checking for Timed Automata
  2011 CAV, Springer, Band: 6806, Seiten: 616 - 632
• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
  Integration of orthogonal QBF solving techniques
  2011 DATE, IEEE, Seiten: 149 - 154

2010

 nach oben zur Jahresübersicht

• Florian Pigorsch, Christoph Scholl
  An AIG-Based QBF-solver using SAT for preprocessing
  2010 DAC, ACM, Seiten: 170 - 175

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
• Florian Pigorsch, Christoph Scholl
  Exploiting structure in an AIG based QBF solver
  2009 DATE, IEEE, Seiten: 1596 - 1601
• Florian Pigorsch, Christoph Scholl
  Using Implications for Optimizing State Set Representations of Linear Hybrid Systems
  2009 MBMV, Seiten: 77 - 86

2008

 nach oben zur Jahresübersicht

• 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

• 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.