Seminar: Decision Procedures (CPSC 729a)Information
OverviewThe term "decision procedures" is widely used to describe an algorithm that takes as an input a formula belonging to a certain logic, such as linear integer arithmetic, bit vectors, or real numbers. A decision procedure checks if the input formula has a model, i.e. if there is an assignment to its variables such that the input formula evaluates to truth. If a formula has a model, we say the formula is satisfiable. Otherwise we call such a formula unsatisfiable. In an ideal case, the decision procedure returns either a model of the input formula or a proof of its unsatisfiability. In recent years we have witnessed an increased interest in decision procedures and SMT solvers, both in academic and industrial research. A SMT (satisfiability modulo theories) solver is a tool that implements decision procedures. SMT solvers are one of the most important ingredients of many tools used in software and hardware verification. This course will describe the ideas based on which modern SMT solvers are built. We will describe their basic architecture and cover many interesting decision procedures used in verification. The course will be organized as a seminar, consisting of presentations given by the course instructor and the course participants. We will meet once a week, for two hours. There will not be any homework, however the seminar will thrive on lively discussions, in which you are expected to participate. Due to prescheduled traveling of the course instructor, there will be three weeks without the classes, which will will be rescheduled to some other time. Course MaterialThe seminar is based on:
Slides |