Credit Level: U. Credit Hrs: 3.00.
Prerequisites: 20-CS-229

An introduction to formal hardware and software verification. Two approaches are introduced: model checking and logical inference. Tools and representations based on these techniques are applied to specific formal verification problems. Tools discussed are: SAT solvers, SMT solvers, ACL2, ABC, and Cryptol. Representations discussed are CNF propositional formulas, first order logic, and and-inverter graphs. Examples of problems verified range from sorting algorithms such as mergesort to encryption algorithms such as AES.

Hardware verification, software verification, concrete simulation, symbolic simulation, concolic simulation, model checking, logical inference, propositional formulas, and-inverter graphs, first order logic, equivalence checking, ACL2, SAT solver, SMT solver, ABC, Cryptol, 3DES, AES.