An attempt to apply formal methods (D. Gries style) to specification and verification of code-writting tasks for CS students.

Visualised process of the weakest precondition's computing

A repository that describes my explorations on formal verification using Dafny, techniques from programming language theory such as CYK parsing, Earley parsing, type-theoretic things like lambda calculus etc.

Concolic Weakest Precondition as a Lens ¯\_(ツ)_/¯

Isabelle/HOL theories for the paper "Backwards and Forwards with Separation Logic".

The goal of this project is to bring most of Event-B and refinement calculus into Python