University of Cincinnati Logo
 

20-CS-626 - Formal Methods
School of Computing Sciences and Informatics

Instructor

John Franco

Registration Data

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

Logistics

Course Description

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.

Keywords

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.

Addendum

ERC
MainStreet
Paul Erdos
NIT
Ladies on Campus
Oscar Robinson