MIRA ist ein vollstaendiger Algorithmus zum Loesen des propositionalen SAT Problemes. Die Kernelemente - basierend auf Ideen von SAT-Prozeduren wie zChaff, Berkmin oder auch Siege - sind hierbei Konfliktanalyse, Watched Literals und diverse Heuristiken zur Auswahl der jeweils naechsten Entscheidungsvariablen. Aufbauend auf diesen (Standard-)Techniken wird MIRA durch weitergehende, leistungsfaehige Funktionen komplettiert: Implication Queue Sorting (IQS), Early Conflict Detection Based BCP (ECDB) sowie eine sich dynamisch anpassende Kombination der verschiedenen zur Verfuegung stehenden Auswahlheuristiken. Durch die Integration aller vorgenannter Strategien ist MIRA in der Lage, die benoetigte Rechenzeit zur Loesung zahlreicher Probleme (z.B. BMC-Benchmarks sowie andere Industrie-Benchmarks) erheblich zu reduzieren.

• M. Lewis, T. Schubert, and B. Becker. "Early Conflict Detection Based BCP for SAT Solving". In "7th International Conference on Theory and Applications of Satisfiability Testing", 2004.
• M. Lewis, T. Schubert, and B. Becker. "Speedup Techniques utilized in Modern SAT Solvers - An Analysis in the MIRA Environment". In "8th International Conference on Theory and Applications of Satisfiability Testing", 2005.

Kontakt: Matthew Lewis

PICHAFF ist ein leistungsstarker paralleler SAT Algorithmus, der speziell fuer Microchip PIC17C43 Mikroprozessoren entwickelt wurde. Alle Funktionen wie beispielsweise Konflikt-Analyse, nicht-chronologisches Backtracking oder auch das Entfernen von gelernten Klauseln sind hierbei an die gegebenen Eigenschaften der Prozessoren angepasst und optimiert worden. Zur weiteren Leistungssteigerung des parallelen Algorithmus ist der Austausch von relevanten Informationen zwischen den einzelnen Prozessoren, die unterschiedliche Teilbereiche des Gesamtproblemes analysieren, moeglich.

Die in diesem Projekt verwendete Hardware-Umgebung ist ein am Lehrstuhl fuer Rechnerarchitektur entwickeltes Multiprozessorsystem, das auf ISA-Steckkarten beruht, die jeweils ueber maximal 9 PIC Prozessoren verfuegen. Zwischen diesen Prozessoren kann die Kommunikationsstruktur jederzeit - insbesondere waehrend des Betriebes - geaendert und somit alle Prozessoren beliebig miteinander verknuepft werden.

• T. Schubert and B. Becker. "PICHAFF2 - A Hierarchical Parallel SAT Solver". In "5th International Workshop on Microprocessor Test and Verification", 2004.
• T. Schubert and B. Becker. "Knowledge Sharing in a Microntroller based Parallel SAT Solver". In "International Conference on Parallel and Distributed Processing Techniques and Applications", 2005.

Kontakt: Tobias Schubert

And-Inverter-Graphen (AIGs) sind eine schaltkreisorientierte Repraesentation boolescher Funktionen, die es erlauben, strukturelle Eigenschaften des zugrundeliegenden Systems zu erhalten. Sie erlauben weiterhin die Anwendungen von dedizierten SAT-Solvern, die direkt auf dem AIG arbeiten, anstatt wie ueblich auf einer klassischen CNF-Darstellung des Problems.

Anwendung findet diese Methodik zum Beispiel beim Bounded Model Checking (BMC). Hierbei wird eine endliche Abwicklung des zugrundeliegenden Systems betrachtet und geprueft, ob ein fehlerhafter Zustand erreichbar ist. BMC ist dabei also eine Methode zur Falsifizierung von Eigenschaften. AIGs koennen beim BMC benutzt werden, um effizient die Abwicklung des Systems darzustellen, und mittels des dedizierten SAT-Solvers das zum BMC korrespondierenden Erfuellbarkeitsproblem zu loesen.

Kontakt: Marc Herbstritt

Viele praktisch relevante Optimierungsprobleme lassen sich als ganzzahliges lineares Optimierungsproblem (ILP) formulieren. Es gibt jedoch heutzutage noch relativ kleine ILPs, die von den aktuellen Solvern nur mit großem Zeitaufwand gelöst werden können. Die Effizienz der Solver hängt stark davon ab, ob gute Schnittebenen gefunden werden, die den Suchraum verkleinern.

Indem wir eine Überapproximation der gültigen Lösungen mittels OBDDs darstellen, wollen wir ein effizientes Verfahren entwickeln, um gute Schnittebenen (wünschenswert sind Facetten des ILP-Polytops) zu finden und so die Lösung von kleinen, aber schweren ILPs zu beschleunigen.

Die Arbeiten finden statt in Kooperation mit Fritz Eisenbrand, Markus Behle (MPI Saarbruecken)

• BDD in a Branch and Cut Framework 4th International Workshop on Efficient and Experimental Algorithms LNCS 3503, 2005

Kontakt: Ralf Wimmer

Visualisierung im Schaltkreisdesign stellt bei der Entwicklung neuer Schaltkreise derzeit die intuitivste Schnittstelle zwischen Mensch und Maschine dar. Die zweidimensionale Darstellung von Schaltungelementen und ihrer Verbindungen unterstützt und beschleunigt sowohl den Entwurf als auch den Diagnoseprozess, da Menschen diese Darstellung gut erfassen können. Um die Benutzbarkeit automatisch erstellter Schaltkreisvisualisierungen zu gewährleisten, ist der Entwurf und die Implementierung von effizienten Algorithmen entscheidend. Weitere wichtige Anwendungen sind die Präsentation und Dokumentation der fertigen Schaltungen, wobei hier insbesondere die Qualität der Visualisierung im Vordergrund steht.

• T. Eschbach, W. Günther, B. Becker. " Orthogonal Circuit Visualization Improved by Merging the Placement and Routing Phases". In "VLSI Design 2005 (VLSID'05)", 2005.
• T. Eschbach, W. Günther, B. Becker. "Orthogonal Hypergraph Routing for Improved Visibility". In "2004 Great Lakes Symposium on VLSI (GLSVLSI'04)", 2004.

Kontakt: Thomas Eschbach

In der Logik der ersten Stufe über gemischter ganzzahliger und reellwertiger Addition, d.h. über der Struktur (ℝ, ℤ, +, <), lassen sich einige Klassen interessanter Systeme beschreiben. Darunter fallen sogenannte lineare hybride Automaten, also Systeme die sowohl aus digitalen als auch aus analogen Komponenten bestehen. Die Analyse solcher Systeme erfordert eine effiziente Entscheidungsprozedur für die Logik, in der die Systeme modelliert sind.

Wir entscheiden diese Logik mit Hilfe von Automaten, indem wir Automaten konstruieren, die alle erfüllenden Belegungen darstellen. Da die binäre Darstellung reeller Zahlen unendlich lang ist, verwenden wir Automaten über unendlichen sogenannten ω-Wörtern. Man kann zeigen, dass schwache deterministische Büchi Automaten ausreichen, um solche Teilmengen von ℝⁿ zu beschreiben, die in der Logik über (ℝ, ℤ, +, <) beschreibbar sind.

Wir entwickeln eine Bibliothek (LIRA) zur effizienten Darstellung und Manipulation solcher Automaten. Ziel ist es, sowohl theoretische Erkenntnisse zu erzielen, die es erlauben größere System zu analysieren, als auch diese Erkenntnisse in die Praxis umzusetzen.

• J. Eisinger, F. Klaedtke. "Don't care words with an application to the automata-based approach for real addition". In 18th International Conference on Computer Aided Verification. LNCS 4144. pp 67-80. Springer-Verlag, 2006.
• B. Becker, C. Dax, J. Eisinger, F. Klaedtke. "LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals". In 19th International Conference on Computer Aided Verification. LNCS 4590. pp 312-315. Springer-Verlag, 2007.
• C. Dax, J. Eisinger, F. Klaedtke. "Mechanizing the Powerset Construction for Restricted Classes of ω-Automata". In 5th International Symposium on Automated Technology for Verification and Analysis. LNCS 4762. pp 223-236. Springer-Verlag, 2007.

Bounded model checking (BMC) ist eine Technik um Berechnungen eines Systems zu finden, die die S pezifikation verletzen. Die Existenz solcher Berechnungen bestimmter Laenge werden durch logische Formeln beschrieben. Diese Formeln koennen dann mit Hilfe von SAT-Solvern fuer binaere und SAT-LP-Solvern fuer hybride diskret-kontinuierliche Systeme mit linearem Verhalten auf Erfuellbarkeit getestet werden.

Unser Forschungsvorhaben ist die Entwicklung von einem, speziell auf das BMC-Problem von linearen hybriden Systemen angepassten SAT-LP-Solver. Nicht-lineare hybride Systeme werden auf ueberapproximierende Weise linearisiert. Gegenbeispiele in der Abstraktion, die keiner Berechnung im konkreten System entspechen, werden verwendet um die Abstraktion zu verfeinern. Duch die Bestimmung von Terminierungsbedingungen kann BMC auch als Verifikationstechnik angewendet werden.

Neben der Optimierung der Solver-Eingabe, d.h., der Kodierung der Berechnungen, werden sowohl die Datenstrukturen als auch die Entscheidungsprozeduren im SAT- und auch im LP-Teil an die stark symmetrische Struktur der Formeln angepasst. Zusaetzlich zu den speziell auf BMC bezogenen Optimierungen beschaeftigen wir uns mit allgemeinen SAT-LP Fragen, z.B. der effizienten Bestimmung von minimal infeasible subsets im LP-Solver.

Die Arbeiten finden statt in Kooperation mit

1. Christian Herde, Martin Fränzle (Oldenburg)
2. Felix Klaedtke (Zürich)
3. Martin Steffen (Kiel)

• E. Abraham, M. Herbstritt, B. Becker, M. Steffen, "Bounded Model Checking with Parametric Data Structures", In Proceedings of Fourth International Workshop on Bounded Model Checking (BMC), Seattle, USA, August 15. 2006. to appear
• E. Abraham and B. Becker and F. Klaedtke and M. Steffen, "Optimizing Bounded Model Checking for Linear Hybrid Systems",6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2005), pp.396--412, 2005.

Kontakt: Erika Abraham

Die symbolische Modellprüfung (Symbolic Model Checking) ist seit Jahren ein etabliertes Verfahren im Bereich der automatischen Verifikation von Systemen zum Beweis von Eigenschaften (gegeben einer temporalen Logik), es ist jedoch (üblicherweise) nur in der Lage, vollständig beschriebene Systeme zu verifizieren.

Noch nicht vollständige Systeme (etwa in der frühen Entwurfsphase) und Systeme, in denen aus Diagnosegründen Teile ausgeblendet wurden, können mit der klassischen Modellprüfung nicht behandelt werden. Diese nicht spezifizierten Teile des Systems werden als "Black Boxes" bezeichnet.

Unsere Forschungen im Bereich Black-Box Model Checking erweitern die Verfahren der symbolischen Modellprüfung um die Möglichkeit, auch solche unvollständig spezifizerten Designs zu behandeln.

Da ein vollständiges Verfahren eine hohe Komplexität besitzt oder gar unentscheidbar sein kann, wird eine Reihe von verschiedenen approximativen Verfahren mit unterschiedlicher Präzision, aber auch Komplexität entwickelt. Weitere Details zu den einzelnen Verfahren finden sich hier.

Bei der Implementierung der einzelnen Verfahren kommt es wesentlich auf die gewählte Datenstruktur und die durch sie zur Verfügung gestellten Operationen an: so ist es allgemein bekannt, dass selbst bei klassischem Model Checking BDD-basierte Verfahren oft nicht in der Lage sind, heutige Schaltungen zu bearbeiten. Wir untersuchen im Rahmen dieses Projektes deshalb alternative Datenstrukturen (AIGs) zur Umsetzung von (Black-Box) Model Checking.

Kontakt: Stefan Disch

Gerade in der fruehen Entwurfsphase von Systemen geht es darum, fehlerhafte Implementierungen, die notwendige Spezifikationseigenschaften verletzen, frueh zu erkennen. D.h. man moechte z.B. folgende Frage beantworten: "Wird eine Eigenschaft P bereits verletzt, unabhaengig davon wie man die noch nicht implementierten Bereiche (Blackboxes) implementieren wird?".

Hierzu kann die Methode des Bounded Model Checking (BMC) angewendet werden, bei der eine endliche Abwicklung des Systems daraufhin geprueft wird, ob ein fehlerhafter Zustand erreichbar ist. Zusaetzlich zum herkoemmlichen BMC muss nun aber noch die Modellierung der Blackboxes miteinbezogen werden.

Dies fuehrt jedoch dazu, dass man die auftretenden Probleme nicht mehr mit rein booleschen Formeln effizient beschreiben kann, sondern entweder die zugrundeliegende Logik stueckweise erweitern muss (01X) oder aber Quantoren zur Modellierung heranzieht (QBF). Wie beim herkoemmlichen BMC wird auch beim Blackbox BMC versucht, SAT-basierte Algorithmen anzuwenden.

• M. Herbstritt, B. Becker, "On Combining 01X-Logic and QBF", in Proceedings of 11th International Conference on Computer Aided Systems Theory, Applied Formal Verification Track, (EuroCAST 2007), Las Palmas de Gran Canaria, Canary Islands, Spain, February 12-16 2007. Springer LNCS.
• M. Herbstritt, B. Becker, C. Scholl, "Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs", in Proceedings of 7. IEEE International Workshop on Microprocessor Test and Verification (MTV 2006), pp. 37-44, Austin (TX), USA, December 04-05 2006.
• M. Herbstritt, B. Becker, "On Bounded Invariant Checking of Blackbox Designs", in Proceedings of 6. IEEE International Workshop on Microprocessor Test and Verification (MTV 2005), pp. 23-28, Austin (TX), USA, November 03-04 2005.

Kontakt: Marc Herbstritt

Bisimulationen sind eine bewährte Technik, um dem Problem zu begegnen, dass der Zustandraum eines reaktiven Systems zu stark anwächst. Alle Zustände, die in den relevanten Eigenschaften übereinstimmen, werden dabei durch einen einzelnen Zustand ersetzt.

Wenn das reaktive System Aktionen enthält, die entweder aus Benutzersicht nicht beobachtbar oder für die zu verifizierenden Eigenschaften unwesentlich sind ("tau-Aktionen"), kann dies ausgenutzt werden, um das System stärker zu verkleinern.

Unser Ziel ist es, symbolische Algorithmen für die Berechnung solcher Bisimulationen finden, die die tau-Aktionen ausnutzen, um sie auf größere Zustandsräume als bisher anwenden zu können.

• R. Wimmer, M. Herbstritt, B. Becker, "Optimization Techniques for BDD-based Bisimulation Computation", in Proceedings of 17th ACM Great Lakes Symposium on VLSI (GLSVLSI), pp. 405--410, Stresa-Lago Maggiore, Italy, March 11-13 2007. ACM Press.
• R. Wimmer, M. Herbstritt, H. Hermanns, K. Strampp, B. Becker, "Sigref - A Symbolic Bisimulation Tool Box", in Proceedings of 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), Beijing, China, October 23.-26. 2006. Springer LNCS 4218.
• E. Böde, M.Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, R. Wimmer, B. Becker, "Compositional Performability Evaluation for STATEMATE", In Proceedings of 3rd International Conference on the Quantitative Evaluation of SysTems (QEST), Riverside (CA), USA, September 11.-14. 2006. to appear
• R. Wimmer, M. Herbstritt, B. Becker, "Minimization of Large State Spaces using Symbolic Branching Bisimulation", In Proceedings of 9th IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems (DDECS), pp. 9--14, 2006.

Kontakt: Ralf Wimmer, Marc Herbstritt

In Nanoscale-Fertigungstechnologien treten vermehrt Defekte auf, die nur unzureichend von konventionellen Testmethoden abgedeckt werden. Eine wichtige Defektklasse sind Kurzschlüsse mit nicht vernachlässigbarem Widerstand (welche etwa durch sehr kleine Staubpartikel verursacht werden können). Wir beschäftigen uns mit der Modellierung dieser Defekte als resistive Brückenfehler, wobei der Widerstand a priori unbekannt ist.

Wir entwickeln Simulations- und Testmustergenerierungsalgorithmen für diese Fehlerklasse und untersuchen die Effektivität alternativer Testmethoden (Low Voltage, Low Temperature, Iddq) sowie den Einfluss von statistischen Prozessvariationen auf die Testqualität.

Literatur: I. Polian, P. Engelke, M. Renovell, and B. Becker, "Modeling feedback bridging faults with non-zero resistance", Jour. of Electronic Testing: Theory and Applications, pp.57-69, 2005.

Kontakt: Piet Engelke, Ilia Polian