CS477: Formal Methods for Software Development

Every Tuesday and Thursday from 9:30 to 10:45, 1131 Siebel Center

Professor Mahesh Viswanathan
vmahesh@cs.uiuc.edu 3232 Siebel Center

About this course

Formal methods is a term that refers to a diverse collection of techniques, with strong mathematical foundations, that are used to provide assurance about the correctness of software and hardware systems. The course aims to familiarize students interested in software engineering with languages and methods for formal specification, development and verification. More specifically in this semesters offering of the course, the students will be exposed to the foundations and experimental use of 4 tools that are used in verifying systems:

  1. Maude: Declarative programming environment for rapid prototyping based on equational logic.

  2. STeP: A temporal logic theorem prover ( instructions )

  3. nuSMV: A temporal logic model checker

  4. Java MaC: A runtime verification tool that analyzes Java code

The course will expose students to specification languages like equational logic, and temporal logic, analysis methods like theorem proving, term rewriting, model checking and runtime verification, and a diverse collection of tools used in the industry.

There will be about 4 to 8 homeworks that will include machine problems using these tools. There will also be a final exam.