unitb / unitb-semantics Public

Notifications You must be signed in to change notification settings
Fork 1
Star 3

Proof of soundness of the Unit-B refinement calculus

unitb.github.io/

3 stars 1 fork Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 257 Commits
src/unitb		src/unitb
.travis.yml		.travis.yml
Makefile		Makefile
README.md		README.md
leanpkg.toml		leanpkg.toml
run_make		run_make
todo.md		todo.md

Repository files navigation

unitb-semantics

Travis:

Using Lean to

formally verify the proof obligations of Literate Unit-B
verify implementation rules for Unit-B specifications
certify proofs created by Literate Unit-B

About

Proof of soundness of the Unit-B refinement calculus

unitb.github.io/

theorem-proving verification unitb

Custom properties

Report repository

Releases

No releases published

Packages

No packages published

Contributors 2

Languages