aneris
System verification framework
A framework for developing and verifying distributed systems using separation logic
Program logic for developing and verifying distributed systems
33 stars
10 watching
8 forks
Language: Coq
last commit: almost 2 years agocoqdistributed-systemsirisseparation-logic
Related projects:
| Repository | Description | Stars |
|---|---|---|
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 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 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
 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 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
 imdea-software/htt | A verification system for reasoning about sequential heap-manipulating programs using separation logic and dependent types | 70 |
 uwplse/verdi | A framework for formally verifying distributed systems implementations in Coq. | 595 |
 anssi-fr/dfir4vsphere | A PowerShell module for collecting logs and forensics data from VMware vSphere environments. | 143 |
 brexhq/substation | A toolkit for routing, normalizing, and enriching security event logs across the cloud | 332 |
 sri-csl/pvs | A verification system for formal methods and specification languages | 141 |
| 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 |