ECE 750 topic 28 - Computer-aided Reasoning for Software Engineering
Instructor
Professor Vijay Ganesh
Description
Computer-aided reasoning tools, such as SAT/SMT solvers, have had a dramatic impact on software engineering and security in recent years. The key reason for the adoption of solvers in software engineering is the continuous improvement in their performance and expressive power. In this course, we will cover the theory and practice of automated reasoning tools such as conflict-driven clause learning SAT solvers, SMT solvers, model-checkers, and theorem provers. We will also cover applications of automated reasoning tools in diverse areas such as automatic bug finding, symbolic execution, program analysis, programming languages, and formal methods.
The course consists of 3 modules:
- Mathematical logic and complexity theory basics
- Algorithms for SAT/SMT solvers and theorem provers
- Solver-based applications in testing, program analysis, security, and formal methods
Please visit the website for a previous edition of this course.