This course is an introduction to the theory and applications of formal methods, a field of computer science and engineering concerned with the rigorous mathematical specification, design, and verification of systems. At its core, formal methods is about proof: formulating specifications that form proof obligations, designing systems to meet those obligations, and verifying, via algorithmic proof search, that the systems indeed meet their specifications. In particular, the course will cover topics such as model checking, Boolean satisfiability (SAT) solving and satisfiability modulo theories (SMT). These techniques have become essential tools for the design and analysis of hardware, software, and cyber-physical systems. Central themes of the course this year will include (i) the close connections between verification and synthesis, and (ii) the interplay between inductive inference (learning from examples) and deductive reasoning (logical inference and constraint solving). Based on time and interests, we will also cover other current research topics such as combining machine learning and formal methods, formal methods for safe and high assurance artificial intelligence (AI) and robotics, formal methods for building secure systems, formal methods for human-robot (human-CPS) systems, formal methods for education, etc. (Instructor: Prof. Sanjit A. Seshia)

I gave the lectures on Hyperproperties and Runtime Assurance

This course is an introduction to the theory and applications of formal methods, a field of computer science and engineering concerned with the rigorous mathematical specification, design, and verification of systems. At its core, formal methods is about proof: formulating specifications that form proof obligations, designing systems to meet those obligations, and verifying, via algorithmic proof search, that the systems indeed meet their specifications. In particular, the course will cover topics such as model checking, Boolean satisfiability (SAT) solving and satisfiability modulo theories (SMT). These techniques have become essential tools for the design and analysis of hardware, software, and cyber-physical systems. Central themes of the course this year will include (i) the close connections between verification and synthesis, and (ii) the interplay between inductive inference (learning from examples) and deductive reasoning (logical inference and constraint solving). Based on time and interests, we will also cover other current research topics such as combining machine learning and formal methods, formal methods for safe and high assurance artificial intelligence (AI) and robotics, formal methods for building secure systems, formal methods for human-robot (human-CPS) systems, formal methods for education, etc. (Instructor: Prof. Sanjit A. Seshia)

I gave the lectures on Hyperproperties and Runtime Assurance

This course is an introduction to the theory and applications of formal methods, a field of computer science and engineering concerned with the rigorous mathematical specification, design, and verification of systems. At its core, formal methods is about proof: formulating specifications that form proof obligations, designing systems to meet those obligations, and verifying, via algorithmic proof search, that the systems indeed meet their specifications. In particular, the course will cover topics such as model checking, Boolean satisfiability (SAT) solving and satisfiability modulo theories (SMT). These techniques have become essential tools for the design and analysis of hardware, software, and cyber-physical systems. Central themes of the course this year will include (i) the close connections between verification and synthesis, and (ii) the interplay between inductive inference (learning from examples) and deductive reasoning (logical inference and constraint solving). Based on time and interests, we will also cover other current research topics such as combining machine learning and formal methods, formal methods for safe and high assurance artificial intelligence (AI) and robotics, formal methods for building secure systems, formal methods for human-robot (human-CPS) systems, formal methods for education, etc. (Instructor: Prof. Sanjit A. Seshia)

I gave the lectures on Temporal Logocs, Hyperproperties and Runtime Assurance