Due to the growing use of more and more complex computerized systems in the safety-critical applications, the formal verification of such systems is increasingly gaining importance. Many automatic and semi-automatic schemes for hardware and software verification ultimately rely on decision procedures for discharging the proof obligations generated during the verification process. Christian Herde deals with the development of such procedures, providing 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. Although aiming at providing tool support for the verification of hybrid discrete-continuous systems, most of the techniques he describes are general purpose and have applications in many other domains, like operations research, planning, software validation, and electronic design automation.
Author(s): Christian Herde
Publisher: Vieweg+Teubner
Year: 2011
Language: English
Pages: 182
Tags: Математика;Методы оптимизации;
Cover......Page 1
Efficient Solving
of Large Arithmetic Constraint
Systems with Complex Boolean
Structure......Page 4
ISBN 9783834814944......Page 5
Foreword......Page 6
Acknowledgements......Page 8
Abstract......Page 10
Zusammenfassung......Page 12
Contents......Page 14
List of Figures......Page 16
List of Tables......Page 18
1.1 Formal Verification Using Satisfiability Checking......Page 20
1.2 Bounded Model Checking of Hybrid Systems......Page 22
1.3 Solvers for Boolean Combinations of Numerical Constraints......Page 24
1.3.1 Constraint Solving in a Nutshell......Page 25
1.3.2 Contributions of the Thesis......Page 28
1.3.4 Sources......Page 31
2 Hybrid Dynamical Systems......Page 34
2.1 Modeling Hybrid Systems with Hybrid Automata......Page 35
2.2 Predicative Encodings of Hybrid Automata......Page 42
2.2.1 A Basic Encoding Scheme......Page 43
2.2.2 Hybridization of Continuous Dynamics......Page 49
2.2.3 Encoding Flows Using Taylor Expansions......Page 52
3 Extending DPLL for Pseudo-Boolean Constraints......Page 56
3.1 The Logics......Page 58
3.2 State of the Art in SAT Solving......Page 59
3.2.1 Conversion into CNF......Page 61
3.2.2 SAT Checkers for CNFs......Page 64
3.3 Optimizing DPLL-Based Pseudo-Boolean Solvers......Page 68
3.3.1 DPLL for Pseudo-Boolean Constraints......Page 69
3.3.2 Generalization of Lazy Clause Evaluation......Page 70
3.3.3 Learning in Presence of Pseudo-Boolean Constraints......Page 72
3.4 Benchmark Results......Page 74
3.5 Discussion......Page 76
4 Integration of DPLL-SAT and Linear Programming......Page 78
4.1 The Logics......Page 79
4.2 Lazy Approach to SMT......Page 81
4.3 SAT Modulo the Theory of Linear Arithmetic......Page 82
4.3.2 Extractions of Explanations......Page 84
4.3.4 Putting It All Together: a Sample Run......Page 87
4.4 Optimizations for BMC......Page 89
4.5 Benchmark Results......Page 91
4.6 Discussion......Page 93
5 Integration of DPLL and Interval Constraint Solving......Page 100
5.1 The Logics......Page 104
5.2 Algorithmic Basis......Page 107
5.3.1 Definitional Translation into Conjunctive Form......Page 109
5.3.2 Split-and-Deduce Search......Page 113
5.3.3 Arithmetic Deduction Rules......Page 117
5.3.4 Correctness......Page 123
5.3.5 Algorithmic Enhancements......Page 128
5.3.6 Progress and Termination......Page 131
5.4.1 Impact of Conflict-Driven Learning......Page 133
5.4.2 Comparison to ABSOLVER......Page 134
5.5 Reachability Analysis with HYSAT-2: a Case Study......Page 138
5.5.1 ETCS Model......Page 139
5.5.2 Encoding into HySAT......Page 143
5.5.3 Results......Page 147
5.6 Discussion......Page 149
6.1 Achievements......Page 152
6.2 Perspectives......Page 154
6.3 Final Thoughts......Page 162
Bibliography......Page 164
C......Page 178
I......Page 179
P......Page 180
T......Page 181
Z......Page 182
