Zur Seitenansicht
 

Titelaufnahme

Titel
Bit-Precise Reasoning Beyond Bit-Blasting / eingereicht von Dipl.-Ing. Aina Niemetz, Bsc
VerfasserNiemetz, Aina
Begutachter / BegutachterinBiere, Armin ; Barrett, Clark
GutachterBiere, Armin
ErschienenLinz, Februar 2017
Umfangxii, 163 Seiten : Illustrationen
HochschulschriftUniversität Linz, Dissertation, 2017
Anmerkung
Zusammenfassung in deutscher Sprache
SpracheEnglisch
Bibl. ReferenzOeBB
DokumenttypDissertation
Schlagwörter (DE)Satisfiability Modulo Theories / formale Verifikation / Entscheidungsprozeduren / Bit-präzise Beweisführung
Schlagwörter (EN)satisfiability modulo theories / bit-precise reasoning / formal verification / decision procedures
Schlagwörter (GND)Prädikatenlogik / Stufe 1 / Erfüllbarkeitsproblem / SMT Solver / Bitvektor / Entscheidungsverfahren
URNurn:nbn:at:at-ubl:1-16820 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist gemäß den "Hinweisen für BenützerInnen" verfügbar
Dateien
Bit-Precise Reasoning Beyond Bit-Blasting [4.05 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

In the field of hardware and software verification, many applications require to determine satisfiability of first-order-logic with respect to one or more back- ground theories, also referred to as Satisfiability Modulo Theories (SMT). The majority of these applications relies on bit-precise reasoning as provided by SMT solvers for the quantifier-free theory of fixed-size bit-vectors, often combined with arrays and uninterpreted functions. Fixed-size bit-vectors provide a natural way to model circuits and programs and arrays allow to reason about memory and array data structures. Uninterpreted functions, on the other hand, are useful as abstraction for irrelevant or too complex details of a system.

In this thesis, our main focus is on SMT procedures for bit-vector logics. In the context of quantifier-free bit-vector formulas in SMT, current state-of-the- art is a flattening technique referred to as bit-blasting, where the input formula is eagerly translated into propositional logic and handed to an underlying SAT solver. While efficient in practice, in particular for increasing bit-widths, bit- blasting may not scale if the input size can not be reduced sufficiently during preprocessing. In this thesis, we propose alternative approaches for bit-vector logics based on local search that do not require bit-blasting or an underlying SAT solver and yield a substantial gain in performance, in particular in combination with bit-blasting within a sequential portfolio setting.

In the context of combining quantifier-free bit-vectors with arrays and unin- terpreted functions, current state-of-the-art SMT procedures are based on lazy rather than eager techniques. One such lazy technique is the Lemmas on Demand (LOD) approach, which refines full candidate models of a formula abstraction with lemmas until convergence. Full candidate models, however, include irrele- vant parts of the input formula, which may introduce unnecessary overhead. In this thesis, we propose an optimization of LOD where focusing refinement on relevant parts of the input formula considerably improves performance.

We implemented all of our techniques within our SMT solver Boolector, which contributed to Boolector winning several tracks of recent SMT competitions. Boolector supports the quantifier-free theories of fixed-size bit-vectors, arrays and uninterpreted functions and natively handles non-recursive first-order lambda terms. It is a complex piece of software with correctness, robustness and high performance as its key requirements. and in this thesis, we address automated testing and debugging techniques for SMT solver development that we consider as crucial to reach this goal.

Zusammenfassung (Deutsch)

Eine Vielzahl an Applikationen im Bereich der formalen Verifikation von Hard- ware und Software erfordert das Lösen des Erfüllbarkeitsproblem der Prädikaten- logik erster Stufe unter Berücksichtigung einer oder mehrerer Theorien, auch bekannt als Satisfiability Modulo Theories (SMT), und setzt dafür auf SMT- Prozeduren (sogenannte SMT-Solver) für die quantorenfreien Theorien der Bit- vektoren, Arrays und nicht-interpretierten Funktionen. Die bisher gebräuchliste und in der Praxis effizienteste Technik für das Lösen von quantorenfreien Bitvektorformeln ist “Bit-Blasting”, das eine gegebene Formel in ein Entscheidungsproblem der Aussagenlogik (SAT) übersetzt und an einen SAT-Solver delegiert. Für hohe Bitweiten kann es jedoch sein, dass Bit-Blasting nicht skaliert wenn es dem Präprozessor nicht gelingt die gegebene Formel ausre- ichend zu vereinfachen bevor sie nach SAT übersetzt wird. Wir stellen eine Meth- ode vor, Bitvektorformeln in SMT ohne Bit-Blasting zu lösen, die auf lokaler Suche basiert, und insbesondere in Kombination mit Bit-Blasting in einem so genannten sequentiellen Portolio eine erhebliche Leistungsverbesserung erzielt.

Aktuell gebräuchliche Prozeduren für das Lösen von Bitvektorformeln, die Arrays und nicht-interpretierte Funktionen enthalten, sind im Gegensatz zu Bit- Blasting keine direkten Übersetzungen nach SAT, sondern basieren auf Ansätzen, die eine Abstraktion der gegebenen Formel iterativ verfeinern. Ein Beispiel dafür ist die “Lemmas on Demand” (LOD) Technik, die vollständige Modelle der Formelabstraktion mit Lemmas verfeinert bis Erfüllbarkeit oder Nichterfüll- barkeit nachgewiesen werden kann. Vollständige Modelle enthalten jedoch auch irrelevante Teile der Formelabstraktion, was unnötigen Overhead erzeugen kann. Wir stellen eine Optimierung von LOD vor, die nur relevante Teile der Forme- labstraktion berücksichtigt und damit die Leistung deutlich verbessert.

Wir haben alle unsere Techniken in unserem SMT-Solver Boolector imple- mentiert, was erheblich dazu beigetragen hat, dass Boolector mehrere Tracks der SMT Competitions der letzten Jahre gewonnen hat. Boolector ist ein SMT- Solver für die quantorenfreien Theorien der Bitvektoren, Arrays und nicht-inter- pretierten Funktionen und bietet darüberhinhaus native Unterstützung für nicht- rekursive Lambdaterme erster Ordnung. Boolector ist ein komplexes Tool, das in erster Linie als Backend eingebunden wird, und als Hauptanforderungen Kor- rektheit, Robustheit und hohe Performanz erfüllen muss. Wir stellen automa- tisierte Test- und Debugging-Techniken für die SMT-Solverentwicklung vor, die wesentlich dazu beigetragen haben diese Ziele zu erreichen.