Instructor: Professor Kristin Yvonne Rozier
Office: 0238 Howe Hall
Office hours:
TR 12:30pm--1:30pm
or by appointment

Postdoctoral Lecturer: Dr. Katherine Kosaian
Office hours: by appointment

Guest Lecturer: Christopher Johannsen

Office hours: by appointment

Location: Howe Hall 2228

Meeting Time: TR 11:00am--12:15pm

AERE/COMS 407/507
Applied Formal Methods

Course Summary

In this course you will be introduced to best practices for the application of formal methods, a set of mathematically rigourous techniques for the formal specification, validation, and verification of safety- and security-critical cyberphysical systems, of which aircraft and spacecraft are the prime example. We will explore the tools, techniques, and applications of formal methods, focusing on the aerospace domain. We will examine the latest research to gain an understanding of the current state of the art, including the capabilities and limitations of applying formal methods for systems analysis. Students will leave with a better understanding of real-world system specification, design, and verification, including why the FAA specifically calls out formal methods in certification requirements such as DO-178B, DO-178C, and DO-254, and why modern security teams from DARPA to AWS require formal methods for cloud security.

This course is intended to be a fun, interactive introduction to applying formal analysis in the context of real-world systems. Hands-on learning, through the use of software tools in homeworks and projects, will be emphasized. We will learn the real tools used at NASA, Boeing, Rockwell Collins, Honeywell, Airbus, Amazon, and others. Students from all areas of aerospace engineering, electrical and computer engineering, computer science, cybersecurity, mathematics, and other engineering disciplines, are encouraged to enroll.

Course Syllabus


The prerequisite is mathematical maturity: Calculus II plus familiarity with discrete mathematics (or ability to learn them quickly from review material made available in the course). This prerequisite take the form of a disjunction; one of the following is required: AERE 361, COMS 311, or permission of the instructor.


Spin Model Checker
SPOT Produces Our Traces
nuXmv Model Checker
In addition to the manuals, see the Introduction Slides
Isabelle Theorem Prover
Also: The Isabelle Cookbook and Guide for Beginners; See also Linear Temporal Logic, and Propositional and Modal Logic in Isabelle (also Modal Logics for Nominal Transition Systems), and Hybrid Logics like Epistemic Logic, State Counting/Reduction
PVS Theorem Prover
NASA PVS Library (NASALib) v7.1 (
30+ years of theorem proving at NASA:
PRISM Model Checker
Responsive Realizable Unobtrusive Unit (R2U2)
Dafny Language and Program Verifier
Note that Dafny has many popular video tutorials!
Z3 SMT Solver
See also:
SMT: Something You Must Try
CBMC (Bounded Model Checker for C programs)
Tip: CBMC has little support for C++; use for C only. Use CBMC for "unit proof" starting from the leaves of the call tree and working toward the root call; see Amazon's strategy here:
Coq Proof Assistant
Book: Formal Reasoning About Programs

Software Model Checking
Competition on Software Verification (SV-COMP)
Hardware Model Checking
HardWare Model Checking Competition (HWMCC)
Static Analysis
Static Analysis: An Introduction
ATP (Automated Theorem Proving)
The CADE ATP System Competition: The World Championship for Automated Theorem Proving

Do not struggle with tool installation on your own machine! If you are running linux, these tools should all install easily, but if not, use the provided virtal machines. There is no credit for time spent trying to install a tool. To access tools like spin, you will need to vpn in from off campus and then ssh -X This works from a command line (e.g., in linux), or from mobaXterm in windows. All software (e.g., Isabelle and nuXmv) is installed in /usr/local/packagename, except for spin and ispin, which are in /usr/local/bin. The GUI ispin is invoked by running "ispin.tcl" from the command line. Nathan Vaughn also wrote a blog post about how to get ispin working with windows

Exam Dates (estimated)

Midterm: 10/24

Final Project: (in lieu of final exam)

Project Requirements: HERE
Optional GitHub classroom link: HERE
Project Proposal: 10/26
Project Midterm Report: 11/9 or 11/14 Give short mid-term presentations on this day!
Project Presentations: 12/5:
Friday Progress Reports Due: 11/10, 11/17, 11/24 (optional), 12/1, 12/8
Final Report: During exam period (9:45am-11:45am on Wednesday, 12/13)

Assignment Deadlines

Homework 0 due 8/24

Homework 1 due 8/31

Homework 2 due 9/12

Homework 3 due 9/28

Homework 4 due 10/10

Homework 5 due 10/17

Update: There will be a total of 5 homeworks. There is no Homework 6.

Choice of research paper for in-class presentation due 10/17


Homework 0 (Review of Version Control and LaTeX primer): distributed 8/22 from HERE

Note: if you want a deeper understanding of git, there are many online courses.

Homework 1 (Propositional Logic Review): distributed 8/24 from HERE

  • Here is a handy condensed list of definitions here.

Homework 2 (Temporal Logic): distributed 8/31 from HERE

Homework 3: distributed 9/12 from HERE

Homework 4: distributed 9/28. Submit HERE

Homework 5: distributed 10/10 HERE

Choice of research paper for presention due via email: 10/17
You may not choose a paper authored by the professor.

Professor evaluation form for in-class presentations is available HERE
Student evaluation form for in-class presentations is available HERE

Here is some great advice on How to Give a Good Research Presentation.

Here is some great advice on How to Read a Paper (there is also advice on how to write papers).

Paper Presentation Schedule:
Each presentation should be approximately 25 minutes, including time for questions.

10/19 Midterm Examination
10/31 & &
11/ 2 & &
11/ 7 & &
11/ 9Midterm project report presentations
11/14Midterm project report presentations
11/16 & &
11/28 & &
11/30 & &
12/5 Final project report presentations
12/7Final project report presentations
12/13(during final exam period) Final project report presentations

Optional Textbooks

Use this for:
  • good background on LTL: well-formed formulas, semantics, encoding English sentences, expressivity, normal forms, relationship to automata
  • reactive system properties: safety, liveness, fairness
  • specification and modeling of real systems
  • deciding the truth of a temporal formula; related proof techniques including explicit model checking
  • thorough chapter on Spin, including how to run it from the command line and a good Promela tutorial
  • review of classical and propositional logic
  • extensions including synthesizing software from specifications
Be cautious that:
  • LTL is instead called PTL in this book; that is non-standard
  • LTL2BA is not the best tool; SPOT is far superior now:
  • URLs provided are outdated (no longer active or superseded by the state of the art)
  • Spin chapter refers to outdated xspin (though only briefly)

Use this for:
  • supplemental material on temporal logics (LTL, CTL, CTL*)
  • background on automata as system models
  • review of explicit and symbolic model checking
  • reachability, safety, liveness, deadlock-freeness, fairness
  • overview of modeling abstraction methods
  • out-of-date chapters on SPIN and SMV still have useful reviews of basic tool usage
  • ideas for related formal methods, including timed automata models, additional tools
Be cautious that:
  • This book is extremely out of date!
  • LTL is the proper name for Linear Temporal Logic (book calls it PLTL)
  • comparisons of LTL vs CTL/CTL* have been changed/been disproved
  • SMV version described is no longer available; current tool is nuXmv
  • Spin version described has been updated (xspin vs ispin)

LaTeX Resources

Awesome Applications