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: 9 months ago coqiristutorial
Related projects:
Repository | Description | Stars |
---|---|---|
| Mechanized formalization of soundness for DOT with logical relations in Coq | 30 |
| A formalisation of Partial Commutative Monoids (PCMs) for verification of concurrent programs. | 26 |
| Enables efficient development of large numbers of concurrent Common Lisp applications on Unix systems. | 79 |
| Provides interfaces and abstractions for media processing in real-time communications | 5 |
| Development of a promising semantics for relaxed-memory concurrency | 33 |
| Automated verification of higher-order programs using separation logic | 57 |
| A tool for interactive theorem proving and language support in Coq | 153 |
| Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
| Tools for systematically testing Erlang programs for concurrency errors and verifying their absence. | 333 |
| A formally verified serialization library for Coq | 23 |
| Library for defining data validation contracts in dynamically typed languages | 51 |
| Formal verification of Python code using Coq | 30 |
| Formal verification and implementation of RISC-V processor designs using Coq. | 22 |
| This project provides a development environment and software tools for formalizing the semantics of programming languages in the Coq proof assistant. | 21 |