Temporal logic

Linear temporal logic (LTL)

Computation tree logic (CTL)

Temporal Verification

Model checking

CS 256 Formal Methods for Reactive Systems
 Stanford University Winter 2023 This advanced course delves into the complexities of programming concurrent and reactive systems. It provides a firm theoretical foundation for understanding temporal logics like LTL and CTL, and the main verification techniques including deductive and algorithmic. The course necessitates a background in mathematical logic and familiarity with Algol-like languages. Concurrent and reactive systems are parallel programs that maintain an ongoing interaction with their environment. Examples include operating systems, hardware devices, reservation systems, communication protocols, web servers, air traffic and automobile control systems, and, in general, all embedded systems.

Many of these programs play a critical role in the correct operation of equipment and services so that even small program errors can have disastrous consequences, including loss of lives. Yet these programs are notoriously hard to get correct. Programming them is extremely difficult because of the parallelism involved, while exhaustive testing is impossible due to a generally infinite number of distinct environment conditions.

CS256 introduces the logical foundations to reason about these systems. Specification languages include temporal logics — LTL (linear time) and CTL (branching time) — and automata over infinite strings and trees. We concentrate on giving a firm theoretical basis for the most important verification techniques: deductive (theorem proving), algorithmic (model checking), and their (state-of-the-art) combination.  The basics of mathematical logic, such as CS156, CS157, Phil160a, CS103 or equivalent, and familiarity with an Algol-like language (Pascal, C, Java ...) Previous experience with finite-state automata is useful, but not required, for some parts of the course. - Zohar Manna and Amir Pnueli. *Temporal Verification of Reactive Systems: Safety*, Springer 1995. (AKA *The Green Book*)  
     This is the main textbook and contains about 2/3 of the syllabus.
- *Copies of lecture slides* will be given before each lecture and made available on this web site.
- We will suggest additional books and research papers on specific topics (not required) during the course.

CS 256 Formal Methods for Reactive Systems


Parallelism and Distributed Systems

Regular Expressions from Axioms

Induction

Propositional Encodings

SAT Certificates

Contracts

Dynamic Logic

Convergence

DPLL

Blasting & Quantifiers

Data structure

Compositional Reasoning

Predicate transformer semantics

Sound Transformations

Ghosts

Loops

Sequent Calculus

Satisfiability Modulo Theories (SMT)

Semantics

Array (data structure)

Resolution

Equality and Arrays

15-414 Bug Catching: Automated Program Verification Carnegie Mellon University Spring 2022 This course is about software verification, with the goal of writing bug-free code. Students will learn to formalize program correctness, write verified code, and use automated tools for verification. It explores the principles behind verification tools, logical specifications, and deductive reasoning. Previous knowledge in program correctness reasoning is beneficial. High-profile bugs continue to plague the software industry, leading to major problems in the reliability, safety, and security of systems. This course teaches students how to write bug-free code through the process of software verification, which aims to prove the correctness of a program with respect to a mathematical specification. Along the way, students will learn how to:

- Specify correct program behavior
- Prove the correctness of their code
- Use formal semantics to reason about the soundness of proof rules
- Write practical and efficient verified code
- Use decision procedures and model checkers to reduce verification effort

Students will learn the principles and algorithms behind automated verification tools, and understand their practical limitations while gaining experience writing verified, machine-checked code that solves real problems. **Identify and formalize program correctness.** In order to reason about the existence of bugs in code, and ultimately justify their absence, we need to state what it means for the code to be correct. Students will learn how to formalize correctness using logical specifications that give precise meaning to the program's intended behavior.

**Understand how to write correct software from the ground up.** Writing good specifications of program correctness is essential to showing that there aren't any bugs in the code, but it is also useful for writing good code from the start. Students will develop experience reasoning about correctness as they implement functionality, learning how to write code that establishes and preserves properties and invariants needed to meet a target specification.

**Apply rigorous reasoning to program correctness.** Program verification is the process of mathematically proving that all possible behaviors of a given program adhere to its specification. Students will learn how to use deductive reasoning and state space exploration to realize this goal, and gain experience verifying their own code against logical correctness specifications.

**Learn to use automated tools to aid in verification.** Formally verifying real code is challenging, but given the scale of modern software, can also be tedious and labor-intensive. A number of tools exist for automating key parts of the verification process, notably deductive verification tools and model checkers. Students will learn how to use these tools when developing correct software, and gain experience applying them to non-trivial implementations.

**Understand how verification tools work.** Verification tools are not perfect, and will never be able to scale universally to all software development needs. Understanding the principles and techniques that these tools use is necessary for evaluating when it is appropriate to use a particular tool, and for addressing a tool's limitations when they arise in practice.  There is no textbook for this class, and detailed lecture notes will be posted to the website within a few days after each class. Keep in mind that lecture notes may not contain everything we cover in class. Comments and corrections are welcome, please give them to the course staff on Piazza.

15-414 Bug Catching: Automated Program Verification

Software Engineering

Temporal logic

2 courses cover this concept

CS 256 Formal Methods for Reactive Systems

15-414 Bug Catching: Automated Program Verification