aneris
System verification toolkit
A toolset 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: 4 days ago coqdistributed-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 | 442 |
 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 |
 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 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 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 | 69 |
 uwplse/verdi | A framework for formally verifying distributed systems implementations in Coq. | 589 |
 anssi-fr/dfir4vsphere | A PowerShell module for collecting logs and forensics data from VMware vSphere environments. | 140 |
 brexhq/substation | A toolkit for routing, normalizing, and enriching security event logs across the cloud | 329 |
 sri-csl/pvs | A verification system for formal methods research and application | 139 |
| 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 |