Seminar 15 Feb, 2012
Automated program verification using SAT and SMT encodings of
Diophantine constraints
The talk will cover analyses and techniques developed in the course of my thesis, which covered the process of solving termination problems (specifically, standard or relative TRS) using orderings found by solving Diophantine inequality systems, and furthermore heuristically solving these systems using satisfying instances of corresponding SAT or SMT modelings.
Three specific topics will be covered:
- Increasing development efficiency by debugging SAT modelings using the
graphical debugger SATView
- Solving relative termination problems by removing rules on the
condition of proving a weakened finiteness property of a modified
Dependency Pair problem
- Reducing problem search space by using carrier domains restricted to
powers of two or zero, with a completeness result and use of simpler
arithmetic modelings possible with this heuristic
Diophantine constraints
The talk will cover analyses and techniques developed in the course of my thesis, which covered the process of solving termination problems (specifically, standard or relative TRS) using orderings found by solving Diophantine inequality systems, and furthermore heuristically solving these systems using satisfying instances of corresponding SAT or SMT modelings.
Three specific topics will be covered:
- Increasing development efficiency by debugging SAT modelings using the
graphical debugger SATView
- Solving relative termination problems by removing rules on the
condition of proving a weakened finiteness property of a modified
Dependency Pair problem
- Reducing problem search space by using carrier domains restricted to
powers of two or zero, with a completeness result and use of simpler
arithmetic modelings possible with this heuristic
