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

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

Lectures

Formal Methods and Functional Programming

Program Verification:

• Building a First Verifier