Glossary

Hoare logic Predicate transformer Separation logic Verification condition Weakest precondition

Papers

Implicit dynamic frames

Gillian: Compositional Symbolic Execution For All

Jstar: Practical Verification for Java

Viper

Fair stateless model checking

https://muraliadithya.github.io/publications.html

Lectures

Formal Methods and Functional Programming

Program Verification:

• Building a First Verifier

Blogs

Why Writing Correct Software Is Hard

Some notes on Rust, mutable aliasing and formal verification

From Stacks to Trees: A new aliasing model for Rust

Forge: A tool to teach formal methods