iris-simp-lang
Concurrent programming verifier
Instantiates a simple programming language with Iris to verify concurrent separation logic programs
We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
49 stars
4 watching
4 forks
Language: Coq
last commit: 6 months ago coqiristutorial
Related projects:
| Repository | Description | Stars |
|---|---|---|
 blaisorblade/dot-iris | Mechanized formalization of soundness for DOT with logical relations in Coq | 30 |
 imdea-software/fcsl-pcm | Provides formalisation of Partial Commutative Monoids (PCMs) for verification of pointer-manipulating sequential and concurrent programs. | 26 |
 wadehennessey/wcl | Enables efficient development of large numbers of concurrent Common Lisp applications on Unix systems. | 79 |
 sipsorcery-org/sipsorcerymedia.abstractions | Provides interfaces and abstractions for media processing in real-time communications | 5 |
 snu-sf/promising-coq | Development of a promising semantics for relaxed-memory concurrency | 33 |
 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 | 152 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 parapluu/concuerror | An Erlang-based tool to systematically test programs for concurrency errors | 333 |
 uwplse/cheerios | A formally verified serialization library for Coq | 23 |
 fisxoj/sanity-clause | Library for defining data validation contracts in dynamically typed languages | 51 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 sifive/prockami | Formal verification and implementation of RISC-V processor designs using Coq. | 22 |
| 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 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |