-
Notifications
You must be signed in to change notification settings - Fork 0
A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
License
maksym-bortin/a_framework
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
This package contains a formalisation of a framework for modelling, verification and transformation of concurrent imperative programs in the Isabelle/HOL theorem prover, version 2024 (see www.cl.cam.ac.uk/research/hvg/Isabelle and LICENSE for more details). The theoretical foundation is comprehensively presented in the report [https://arxiv.org/abs/2007.02261]. The package comprises the following theory files: - Prelims.thy -- auxiliaries - LA.thy -- abstract and concrete syntax of the framework's language - SmallSteps.thy -- the computational model - Computations.thy -- potential computations and conditions on these - RG.thy -- the setup of a Hoare-style rely/guarantee (R/G) program logic - ProgCorr.thy -- program correspondences - AnnChange.thy -- annotations do not affect program behaviours - Rules_prelims.thy -- auxiliaries for Rules.thy - Rules.thy -- rules of the R/G program logic - AssocR_tactic.thy -- normalisation of sequential compositions to the right (with small examples) - RG_tactics.thy -- a simple VCG using the rules - Parallel_inc.thy -- the 'parallel increment' example - Mutex.thy -- verification of a model of the Peterson's mutual exclusion algorithm Note: processing Rules.thy may take a few moments.
About
A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
Topics
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published