The framework provides tools to automatize canonical tasks, such as verification condition generation, finding appropriate data refinement relations, and refine an executable program to a form that is accepted by the Isabelle/HOL code generator.
This submission comes with a collection of examples and a user-guide, illustrating the usage of the framework.
[2012-04-23] Introduced ordered FOREACH loops
[2012-06] New features REC_rule_arb and RECT_rule_arb allow for generalizing over variables. prepare_code_thms - command extracts code equations for recursion combinators.
[2012-07] New example Nested DFS for emptiness check of Buchi-automata with witness.
New feature fo_rule method to apply resolution using first-order matching. Useful for arg_conf, fun_cong.
[2012-08] Adaptation to ICF v2.
[2012-10-05] Adaptations to include support for Automatic Refinement Framework.
[2013-09] This entry now depends on Automatic Refinement
[2014-06] New feature vc_solve method to solve verification conditions. Maintenace changes VCG-rules for nfoldli, improved setup for FOREACH-loops.
[2014-07] Now defining recursion via flat domain. Dropped many single-valued prerequisites. Changed notion of data refinement. In single-valued case, this matches the old notion. In non-single valued case, the new notion allows for more convenient rules. In particular, the new definitions allow for projecting away ghost variables as a refinement step.
[2014-11] New features le-or-fail relation (leof), modular reasoning about loop invariants.