Boolean SAT/SMT Solvers for Software Engineering

Спецкурс на английском языке для студентов магистратуры. Лектор курса - профессор университета Ватерлоо (Канада), Виджей Ганеш (Vidjay Ganesh).

Расписание занятий

• Занятия первой части курса: 4,5,7,8 апреля в аудитории 526б, начало в 18:00.
• Занятия второй части курса: будут объявлены позже.

Course annotation

Computer-aided reasoning tools, such as SAT/SMT solvers, have had a dramatic impact on software engineering and security in recent years. So much so that a large number of software engineering tools these days are designed primarily using a SAT or SMT solver as a backend. The primary reason for this recent adoption of solvers in software engineering is the continued improvement in their performance and expressive power. For example, over the last 15 years we have seen a 1000x improvement in the performance of conflict-driven clause-learning SAT solvers. Given their foundational importance and impact, it is important for any student wanting to do research in software engineering, security, or mathematics to have a thorough understanding of SAT/SMT solvers and proof assistants. In this course, we will cover the theory and practice of automated reasoning tools such as conflict-driven clause learning SAT solvers, SMT solvers, and their applications. Below find a brief summary of the topics that we will cover in the course. The course consists of 8 lectures of 3 hour each.

Course structure

Week 1 Lectures

• Lecture 1: Boolean logic, the Boolean satisfiability problem, introduction to SAT solvers, an overview of application of SAT solvers to automatic software testing
• Lecture 2: Conflict-driven clause-learning SAT solvers, branching heuristics, and conflict analysis (part I)
• Lecture 3: Conflict-driven clause-learning SAT solvers, branching heuristics, and conflict analysis, programmatic SAT (part II)
• Lecture 4: Application of SAT solvers to symbolic-execution based testing

Week 2 Lectures

• Lecture 5: First-order logic, first-order theories and related SAT problems
• Lecture 6: SMT solvers, DPLL(T), combination of theories
• Lecture 7: Solvers for theories over bit-vectors and arrays
• Lecture 8: Solvers for theories over strings