Congruence Closure

Propositional calculus (Propositional logic)

Deduction in First Order Logic

Simplex Method

CEGAR (Counterexample-Guided Abstraction Refinement)

Davis–Putnam algorithm (DP)

Bit-Vectors

Abstract interpretation

Satisfiability Modulo Theories (SMT)

DPLL algorithm

From SAT (Satisfiability) to SMT

Syntax-Guided Synthesis (SyGuS)

Abstract DPLL

Nelson-Oppen Method

Proofs in SAT (Satisfiability)

Conflict-driven clause learning (CDCL)

Model checking

IC3 (Model Checking Algorithm)

Hoare Calculus

First-order logic

CS 357 Advanced Topics in Formal Methods Stanford University Fall 2019 This course emphasizes SAT and SMT technology and its applications, offering an understanding of theoretical foundations and how to implement a small theory solver. Applications of SAT/SMT technology in the context of verification are also covered. The advanced topics and lack of specified prerequisites suggest this is a high-level course. The course will focus on SAT and SMT technology and their applications. The students will learn the theoretical foundations of SAT/SMT, how to use SAT/SMT technology to solve problems, and finally how to implement a small theory solver of their own. The course will build up towards various applications of SAT/SMT technology in the context of verification.   **Textbook**:None; research papers will be assigned as weekly reading.

CS 357 Advanced Topics in Formal Methods

Theoretical Computer Science

Congruence Closure

1 courses cover this concept

CS 357 Advanced Topics in Formal Methods