Full Description
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.
Contents
Hybrid Dynamical Systems; Extending DPLL for Pseudo-Boolean Constraints; Integration of DPLL-SAT and Linear Programming; Integration of DPLL and Interval Constraint Solving



