fcsl-pcm
Monoid library
Provides formalisation of Partial Commutative Monoids (PCMs) for verification of pointer-manipulating sequential and concurrent programs.
Partial Commutative Monoids
26 stars
11 watching
13 forks
Language: Coq
last commit: 22 days ago
Linked from 2 awesome lists
concurrencycoqcoq-librarypartial-commutative-monoidseparation-logic
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| imdea-software/htt | A verification system for reasoning about sequential heap-manipulating programs using separation logic and dependent types | 69 |
 uwplse/cheerios | A formally verified serialization library for Coq | 23 |
 coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 llee454/functional-algebra | A Coq formalization of abstract algebra using functional programming style | 28 |
 tchajed/iris-simp-lang | Instantiates a simple programming language with Iris to verify concurrent separation logic programs | 49 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 foreverbell/verified | A collection of formalized and provable data structures and algorithms in Coq for educational purposes | 46 |
 magmide/magmide | Creating a programming language and ecosystem to make formal verification and provably correct software development practical and mainstream for working software engineers. | 812 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 354 |
 jklmnn/continuous-verification | Automates Ada software verification with continuous testing and proofing | 9 |