Isabelle/OFMC: Integrating Automated and Interactive Protocol Verification

Isabelle/OFMC connects the Open-source Fixed-point Model-Checker OFMC (developed by Sebastian Mödersheim) with the interactive theorem prover Isabelle/HOL. As such, Isabelle/OFMC bridges the gap between interactive and automated protocol verification.

Isabelle/OFMC is free software; you can redistribute it and/or modify it under the terms of a BSD-style licence. It is developed by Achim D. Brucker.


isabelle-ofmc-0.0.tgz (ca. 326 KiB, MD5: 6531ef606737ccfa9b0ee216f32b8455, 2009-11-02) ChangeLog

Related Publications