htt
Verification framework
A verification system for reasoning about sequential heap-manipulating programs using separation logic and dependent types
Hoare Type Theory
70 stars
8 watching
5 forks
Language: Coq
last commit: almost 2 years agoLinked from 2 awesome lists
coqhoare-logichoare-monadslinked-listseparation-logictype-system
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| imdea-software/fcsl-pcm | A formalisation of Partial Commutative Monoids (PCMs) for verification of concurrent programs. | 26 |
 magmide/magmide | Creating a programming language and ecosystem to make formal verification and provably correct software development practical and mainstream for working software engineers. | 810 |
 distributedcomponents/disel | A framework for implementing and verifying distributed systems using Coq | 95 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 logsem/aneris | A framework for developing and verifying distributed systems using separation logic | 33 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
| xavierleroy/cdf-sem-meca | This project provides a development environment and software tools for formalizing the semantics of programming languages in the Coq proof assistant. | 21 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
 ssprove/ssprove | A foundational framework for modular cryptographic proofs in Coq | 56 |
 lthms/freespec | A framework for specifying and verifying impure computations in a formal proof assistant | 52 |
 querycert/qcert | A framework for developing and verifying domain-specific languages with a focus on compiler correctness and verification. | 56 |
 verifytests/verify.assertions | An assertion framework that allows developers to interrogate data structures during serialization for verification purposes. | 0 |
 uwplse/verdi | A framework for formally verifying distributed systems implementations in Coq. | 595 |