Literatur für das Seminar Verifikation und Fehlerdiagnose

• Debugging
  • Einfache Gegenbeispiele (Bernhard Zimmermann, Betreuer: Nopper)
    • Grundlagen SAT, BMC
    • Ravi, Somenzi: Minimal Assignments for Bounded Model Checking
    • Schäfer: Vereinfachen von Gegenbeispielen: Kategorisierung und effiziente Algorithmen
• Abstraktion (1)
  • Model Checking und Abstraktion (Katrin Rohrwasser, Betreuer: Nopper)
    • Grundlagen Symbolic Model Checking
    • Clarke, Grumberg, Long: Model Checking and Abstraction
• Fehlerdiagnose
  • Design Error Diagnosis Based On Verification Techniques (Georg Schulz, Betreuer: Büche)
    • Li, Shao, Li: Design Error Diagnosis Based On Verification Techniques
  • Debugging Sequential Circuits Using Boolean Satisfyability (Jan Markstahler, Betreuer: Büche)
    • Ali et al.: Debugging Sequential Circuits Using Boolean Satisfiability
  • Post-Verifiaction Debugging of Hierarchical Designs (Sven Reimer, Betreuer: Büche)
    • Ali et al.:Post-Verifiaction Debugging of Hierarchical Designs
• Verbesserte Basisialgorithmen und Repräsentationsmöglichkeiten
  • DAG-Aware Circuit Compression for Formal Verificaton (Alexander Kortus, Betreuer: Pigorsch)
    • Bresse, Borälv: DAG-Aware Circuit Compression for Formal Verificaton
  • Applying SAT Methods in Unbounded Symbolic Model Checking (Markus Fuchs, Betreuer: Pigorsch)
    • McMillan: Applying SAT Methods in Unbounded symbolic Model Checking
• Abstraktion (2)
  • Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories (Christian Miller, Betreuer: Nopper)
    • Seger, Bryant: Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories
  • Uninterpreted Functions (Ben Kremer, Betreuer: Nopper)
    • Burch, Dill: Automated Verification of Pipelined Microporcessor Control
    • Goel et al.: BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
    • Bryant, German, Velev: Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic
• Hybrides Systeme
  • SAT mit linearen Constraints (Ahmad Majeed, Betreuer: Disch)
    • Audemard et al.: A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematic Propositions
    • Fränzle, Herde: HySAT: Efficient Proof Enginges for Bounded Model Checking of Hybrid Systems