Automated logical reasoning has enabled substantial progress in many fields, including hardware and software verification, theorem-proving, and artificial in- telligence. Different application scenarios may require different automated rea- soning techniques and sometimes their combination. In this course, we will study widely-used logical theories as well as algorithms for answering whether formu- las in those theories are satisfiable. We will consider state-of-the-art automated reasoning techniques for propositional logic, first-order logic, and various first- order theories, such as linear arithmetic over reals and integers, uninterpreted functions, bit-vectors, and arrays. We will also consider ways to reason about combinations of those theories. Topics include: logical foundations, SAT-solving, techniques for first-order theorem proving, decision procedures for different first- order theories, theory combination, the DPLL(T) framework, and applications of automated reasoning in program analysis and hardware verification. Prerequisites: CS 154 Introduction to the Theory of Computation, or CS106b Programming Abstractions and CS 103 Mathematical Foundations of Computing, or consent of instructor
3 units · Letter or Credit/No Credit
Automated logical reasoning has enabled substantial progress in many fields, including hardware and software verification, theorem-proving, and artificial in- telligence. Different application scenarios may require different automated rea- soning techniques and sometimes their combination. In this course, we will study widely-used logical theories as well as algorithms for answering whether formu- las in those theories are satisfiable. We will consider state-of-the-art automated reasoning techniques for propositional logic, first-order logic, and various first- order theories, such as linear arithmetic over reals and integers, uninterpreted functions, bit-vectors, and arrays. We will also consider ways to reason about combinations of those theories. Topics include: logical foundations, SAT-solving, techniques for first-order theorem proving, decision procedures for different first- order theories, theory combination, the DPLL(T) framework, and applications of automated reasoning in program analysis and hardware verification. Prerequisites: CS154 Introduction to the Theory of Computation, or CS106b Programming Abstractions and CS103 Mathematical Foundations of Computing, or consent of instructor