Satisfiability Modulo Theories in Planning and Verification
Master topics which use SMT technology for optimization and verification problems in planning and program verification
Satisfiability modulo theories is an exciting technology which uses logic (specifically, sat solving) to find solutions to decision problems for logical formulas. An emerging application domain for SMT solvers is optimisation, where SMT proposes a new and different technology compared to traditional methods such as, e.g., linear programming and constraint programming. Another is program verification, where SMT offers advanced automated proving.
Several Master topics are available, which explore SMT technology for optimisation and verification:
- Planning problems in collaboration with industry. Examples of possible optimisation problems are: boat schedules, repair of train tracks, hospital patient planning, the cutting stock problem in paper industry.
- Integration of optimisation and executable programs (dynamic symbolic execution). How to integrate symbolic state variables in the simulation engine of the ABS modeling language. Whereas there is a lot of work on dynamic symbolic execution for sequential programs, we are interested in parallel (actor-based) programs.
- Program verification for asynchronous, distributed systems. This topic uses SMT for automated verification of correctness formulas. Relevant background: IN5170 Models of concurrency.