Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure (eBook)

Proof Engines for the Analysis of Hybrid Discrete-Continuous Systems

Christian Herde (Autor)

eBook Download: PDF

2011 | 2011
XVII, 163 Seiten
Vieweg & Teubner (Verlag)
978-3-8348-9949-1 (ISBN)

Infos

Christian Herde deals with the development of decision procedures as needed, e.g., for automatic verification of hardware and software systems via bounded model checking. He provides methods for efficiently solving formulae comprising complex Boolean combinations of linear, polynomial, and transcendental arithmetic constraints, involving thousands of Boolean-, integer-, and real-valued variables.

Dr. Christian Herde completed his doctoral thesis under the supervision of Prof. Dr. Martin Fränzle at the Department of Computing Science at the University of Oldenburg, Germany.

Inhalt

Foreword 6
Acknowledgements 7
Abstract 8
Zusammenfassung 10
Contents 12
List of Figures 14
List of Tables 16
1 Introduction 17
1.1 Formal Verification Using Satisfiability Checking 17
1.2 Bounded Model Checking of Hybrid Systems 19
1.3 Solvers for Boolean Combinations of Numerical Constraints 21
1.3.1 Constraint Solving in a Nutshell 22
1.3.2 Contributions of the Thesis 25
1.3.3 Structure 28
1.3.4 Sources 28
2 Hybrid Dynamical Systems 30
2.1 Modeling Hybrid Systems with Hybrid Automata 31
2.2 Predicative Encodings of Hybrid Automata 38
2.2.1 A Basic Encoding Scheme 39
2.2.2 Hybridization of Continuous Dynamics 45
2.2.3 Encoding Flows Using Taylor Expansions 48
3 Extending DPLL for Pseudo-Boolean Constraints 51
3.1 The Logics 53
3.2 State of the Art in SAT Solving 54
3.2.1 Conversion into CNF 56
3.2.2 SAT Checkers for CNFs 59
3.3 Optimizing DPLL-Based Pseudo-Boolean Solvers 63
3.3.1 DPLL for Pseudo-Boolean Constraints 64
3.3.2 Generalization of Lazy Clause Evaluation 65
3.3.3 Learning in Presence of Pseudo-Boolean Constraints 67
3.4 Benchmark Results 69
3.5 Discussion 71
4 Integration of DPLL-SAT and Linear Programming 73
4.1 The Logics 74
4.2 Lazy Approach to SMT 76
4.3 SAT Modulo the Theory of Linear Arithmetic 77
4.3.1 Feasibility Check Using LP 79
4.3.2 Extractions of Explanations 79
4.3.3 Learning from Feasible LPs 82
4.3.4 Putting It All Together: a Sample Run 82
4.4 Optimizations for BMC 84
4.5 Benchmark Results 86
4.6 Discussion 88
5 Integration of DPLL and Interval Constraint Solving 94
5.1 The Logics 98
5.2 Algorithmic Basis 101
5.3 The ISAT Algorithm 103
5.3.1 Definitional Translation into Conjunctive Form 103
5.3.2 Split-and-Deduce Search 107
5.3.3 Arithmetic Deduction Rules 111
5.3.4 Correctness 117
5.3.5 Algorithmic Enhancements 122
5.3.6 Progress and Termination 125
5.4 Benchmark Results 127
5.4.1 Impact of Conflict-Driven Learning 127
5.4.2 Comparison to ABSOLVER 128
5.4.3 Comparison to HYSAT-1 132
5.5 Reachability Analysis with HYSAT-2: a Case Study 132
5.5.1 ETCS Model 133
5.5.2 Encoding into HySAT 137
5.5.3 Results 141
5.6 Discussion 143
6 Conclusion 145
6.1 Achievements 145
6.2 Perspectives 147
6.3 Final Thoughts 155
Bibliography 157
Index 171

Produkt-Details

• Erscheint lt. Verlag: 29.3.2011
• Zusatzinfo: XVII, 163 p. 30 illus.
• Verlagsort: Wiesbaden
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik
• Schlagworte: Constraint Solving • Formal Verification • Hybrid Systems • Model Checking • satisfiability checking
• ISBN-10: 3-8348-9949-6 / 3834899496
• ISBN-13: 978-3-8348-9949-1 / 9783834899491