Lecturer and scientist. Research area: automated software testing, AI enhanced testing, program verification. Projects:
WLP-based verification
Some previous work I did in verification engines for imperative core-languages. E.g. the Ecore library provides Dijkstra WLP-logic for a simple sequential language. The language supports basic control structures, block, program call (with pass-by-value and pass-by-reference parameters), and "old" key-word in the specification to refer to a variable's initial value. Ecore is provided as a HOL library, thus using HOL as its back-end prover. [download]
UNITY
UNITY is a nice and simple axiomatic formal system by Chandy and Misra used to model concurrent systems and to prove temporal properties about them. See Parallel Program Design: A Foundation" by Chandy, K. Mani and Misra, Jayadev. They had a group at University of Texas at Austin; if for historical reason you are interested in the old collection of "Notes on Unity", they are kept in Misra webpage here.