ECE 750 Topic 28 - Computer-Aided Reasoning for Software Engineering
Instructor
Professor Vijay Ganesh
Course Philosophy and Purpose
Many of our PhD, MaSc and MEng students work in software engineering and computer security related topics. In recent years, automated reasoning tools have become central to many solutions to security and software engineering problems. Hence, a deeper understanding of automated reasoning tools and related theoretical concepts will go a long way in preparing these students for their graduate work and future employment. The purpose of this course is to give students a deeper understanding of the following topics integral to automated reasoning: 1) foundational concepts from mathematical logic, 2) Design and implementation of important automated reasoning algorithms, 3) Applications such bug-finding and formal methods. The course philosophy is “theory and practice together”.
Calendar Description
This course discusses the theory and practice of automated reasoning algorithms such as conflict-driven clause-learning SAT solvers, and their application in software engineering and security. Students will learn theory (logic and complexity theoretic aspects of automated reasoning problem such as the SAT and SMT problem) and application of automated reasoning techniques. Main topics include: 1) fundamental concepts such as the satisfiability/validity problem for various mathematical logic theories useful in software engineering, their complexity, different types of reductions, basic logic concepts such as compactness, soundness, completeness, termination and proof systems; 2) important automated reasoning tools such SAT/SMT solvers, theorem provers, and solver-based model-checking; 3) application of solvers/provers in formal methods, programming languages, type checking, automatic bug-finding, symbolic analysis, program analysis and synthesis.
Prerequisites
Mathematical logic, algorithms and strong programming ability or permission of the instructor
Grading
Assignments
–
15%
Research
Project
–
35%
Final
Exam
–
50%
Research Project
Yes. A research project related to designing/implementing automated reasoning techniques, and/or their application to software reliability and security. The students will be required to submit a project proposal at the beginning of the term. Towards the end of the term they will be required to demo their project and write a research paper describing what they implemented, their design choices, and results (both theoretical and experimental).
Textbook
Instructor notes and research papers
Rationale
Software reliability and security are universally recognized as one of the most important, interesting and hard problems in computer science today. Automated reasoning tools have had a huge impact on most approaches to improving software reliability and security. Any student wanting to do research in software engineering or work in the industry must have a solid grounding in automated reasoning techniques and their applications.
Topics
Theory and practice of automated reasoning tools such as conflict-driven clause learning SAT solvers, SMT solvers, model-checking and theorem proving. Applications of automated reasoning tools in automatic bug finding (e.g., concolic testing), symbolic execution, program analysis and synthesis, programming languages and formal methods.
Lectures
Assuming each lecture is 1.5 hours long, the course plan is to have 24 lectures. The topics will be divided as follows:
- 4 lectures on basic logic concepts such as satisfiability and validity, soundness, completeness, termination of solvers. Introduction to first-order and higher-order logics, compactness, proof systems.
- 2 lectures on complexity theoretic reductions. Important classes such as P, NP etc. Soundness/completeness of reductions. Introduction to parameterized complexity.
- 12 lectures on conflict-driven SAT solving, important SMT solver concepts such DPLL(T) and Nelson-Oppen combintaion, eager vs. lazy methods, local search, proof production by SMT solvers, QBF solvers, solvers for theories of bit-vectors, arrays, strings, uninterpreted functions, integers, reals, Grobner basis.
- 6 lectures on applications such as symbolic analysis and concolic testing, solver-based model checking (IC3 and Interpolant), solvers usage in higher-order theorem provers, program analysis, synthesis, use of solvers in dependent types systems.