Skip to content
/ CVM Public

Code repository for the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant"

License

Notifications You must be signed in to change notification settings

joewatt95/CVM

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Verification of the CVM algorithm

This repository formalises and verifies the CVM algorithm in the Isabelle proof assistant, as presented in the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant".

Project structure

  • isabelle contains the Isabelle sources for our formalisations.
  • paper contains $\LaTeX$ sources for our paper.
  • tools contains miscellaneous tools.
  • archive contains obsolete experiments and formalisations.

About

Code repository for the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant"

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •  

Languages