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 (e.g., for students in other departments). Registering for 407 always requires instructor permission.

	Spin Model Checker http://spinroot.com/ Books: http://spinroot.com/spin/books.html
	SPOT Produces Our Traces https://spot.lrde.epita.fr/
	nuXmv Model Checker https://es-static.fbk.eu/tools/nuxmv/ In addition to the manuals, see the Introduction Slides
	Isabelle Theorem Prover https://isabelle.in.tum.de/ 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 http://pvs.csl.sri.com/ NASA PVS Library (NASALib) v7.1 (https://github.com/nasa/pvslib) NASA PVS VSCode GUI (https://github.com/nasa/vscode-pvs) 30+ years of theorem proving at NASA: https://shemesh.larc.nasa.gov/fm/pvs/
	PRISM Model Checker http://www.prismmodelchecker.org/
	Responsive Realizable Unobtrusive Unit (R2U2) http://temporallogic.org/research/R2U2/
	Dafny Language and Program Verifier http://rise4fun.com/dafny/ https://github.com/dafny-lang/dafny Note that Dafny has many popular video tutorials!
	Z3 SMT Solver https://github.com/Z3Prover/z3 See also: SMT: Something You Must Try
	CBMC (Bounded Model Checker for C programs) http://www.cprover.org/cbmc/ 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: https://nchong.github.io/papers/icse-seip20.pdf
	Coq Proof Assistant https://coq.inria.fr/ 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

Midterm: 10/24

Final Project: (in lieu of final exam)

Homework 0 due 8/29

Homework 1 due 9/5

Homework 2 due 9/17

Homework 3 due 10/3

Homework 4 due 10/15

Homework 5 due 10/24

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

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

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

Homework 1 (Propositional Logic Review): distributed 8/29 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 10/3. Submit HERE

• Proving Theorems With Computers

Homework 5: distributed 10/15 HERE

Choice of research paper for presention due via email: 10/22
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 and how to peer review papers).

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