Boolean SAT/SMT Solvers for Software Engineering

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

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

• Занятия первой части курса: 4,5,7 и 8 апреля 2016 года в аудитории 526б, начало в 18:00.
• Занятия второй части курса: 16 b 17 июня 2016 года в аудитории 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 7 lectures of 3 hour each.

Course projects

• Course projects topics

Course structure

Presentation of course overview

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.
  • Presentation

• Lecture 2: Conflict-driven clause-learning SAT solvers, branching heuristics, and conflict analysis (part I)
  • Presentation - Understanding VSIDS Branching Heuristics in CDCL SAT solvers
  • Presentation - Combining machine learning with deduction for SAT solvers
  • Articles:
  1. Understanding VSIDS Branching Heuristics in CDCL SAT solvers
  2. Learning Rate Based Branching Heuristic for SAT Solvers
  3. Exponential Recency Weighted Average Branching Heuristic for SAT Solvers
• Lecture 3: Conflict-driven clause-learning SAT solvers, branching heuristics, and conflict analysis, programmatic SAT (part II)
  • Articles:
  1. GRASP—A New Search Algorithm for Satisfiability
  2. Impact of Community Structure on SAT Solver Performance
  3. The Quest for Efficient Boolean Satisfiability Solvers
• Lecture 4: Application of SAT solvers to symbolic-execution based testing

Week 2 Lectures

• Lecture 5: Motivation for SMT solvers, and combination of decision procedures.
  • Presentation
• Lecture 6: Combination of decision procedures.
  • Presentation
• Lecture 7: Counterexample-guided abstraction refinement(CEGAR). CEGAR-based SMT solver.
  • Presentation

Brief Bio of Dr. Vijay Ganesh

Official website

Dr. Vijay Ganesh is an assistant professor at the University of Waterloo, Canada, since September 2012. Prior to that he was a Research Scientist at the Massachusetts Institute of Technology (2007-2012), and received his PhD in computer science from Stanford University in 2007. Vijay's primary area of research is the theory and practice of automated reasoning aimed at software engineering, formal methods and security. In this context he has developed many SAT/SMT solvers, most notably, STP, HAMPI, and Z3str2. He has also worked on theoretical results in the context of rich string theories. For his research, he recently won an IBM Research Faculty Award in 2015, two Google Research Faculty Awards in 2013 and 2011, and 7 best paper awards/honors at conferences like SAT, CAV, CADE, and DATE. His solver STP has won numerous awards in highly competitive international SMT solver competitions. Recently he was invited to the first Heidelberg Laureate Forum in 2013, a gathering where young researchers from around the world were selected to meet with leading computer scientists and mathematicians.