Crowfoot

While at University of Sussex I developed the Crowfoot program verifier along with several other researchers. Crowfoot allows the semi-automatic verification of software in which the program itself changes as it executes. This kind of behaviour is found for example in programs which: load and unload code for plugins at runtime, perform runtime code generation, or support “hot updates” where the program can be updated without stopping it running. Such operations are not accounted for by traditional Hoare logic, which assumes the program to be fixed.

You can try Crowfoot online.

HECTOR

The HECTOR program verifier uses the abstract interpretation technique to check assertions and temporal logic properties of programs. The novelty is that HECTOR supports the independent development of a range of state abstraction methods, which can then be “plugged together” as needed for particular verification tasks.

HECTOR is no longer available online, but you can still read about it on my publications page.