cobusve / TLAPLUS_DeadlockEmpireLinks
Specs and models for solving the DeadlockEmpire problems using TLA+ and TLC
☆22Updated 6 years ago
Alternatives and similar repositories for TLAPLUS_DeadlockEmpire
Users that are interested in TLAPLUS_DeadlockEmpire are comparing it to the libraries listed below
Sorting:
- A script for running TLA+/TLC from the command line☆81Updated 4 years ago
- Datalog + Egg = Good☆66Updated 2 years ago
- LVC verified compiler☆58Updated 6 years ago
- Verified hash-based AMQ structures in Coq☆124Updated 5 years ago
- Proving a blocking queue deadlock free in a dozen different ways☆43Updated 11 months ago
- Some fun examples of solving problems with symbolic execution☆115Updated 7 years ago
- Utilities for the TLA+ ecoystem and model-based testing using TLA+.☆28Updated 2 years ago
- Hoare Type Theory☆81Updated 4 months ago
- Very small examples of TLA+ features.☆42Updated 6 years ago
- Synthesis of Heap-Manipulating Programs from Separation Logic☆128Updated 2 years ago
- ☆89Updated 3 years ago
- Foundational Verification of Hybrid Systems☆15Updated 8 years ago
- Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct☆16Updated last year
- Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).☆58Updated 3 years ago
- λ² is a tool for synthesizing functional programs from input-output examples.☆87Updated 2 years ago
- A Rocq formalization of information theory and linear error-correcting codes☆71Updated this week
- Symbolic execution engine for toy language.☆51Updated 7 years ago
- Some unstructured notes concerning the Broad tutorial to take place in March 2020☆32Updated 4 years ago
- CN separation logic refinement type system for C☆38Updated this week
- Unison's source code☆108Updated last year
- Gallina to Bedrock2 compilation toolkit☆61Updated 2 weeks ago
- Online BDD Simulation Tool☆21Updated 2 months ago
- [research] A modular SMT solver in OCaml, based on mcSAT☆39Updated last year
- Logically Qualified Data Types - automatically infer refinement types☆16Updated 4 years ago
- A public repository to host Alloy models. This repository holds public models to be used as entertainment, examples, tutorials, utilitie…☆136Updated 4 months ago
- A model checker for relational first-order temporal specifications☆28Updated 4 years ago
- Repository where I'll collect some demos of proof assistants that I show to various people in order to spread the magic☆38Updated 2 years ago
- Symbolic formula representation and solver interaction library☆169Updated this week
- Haskell re-implementation of STOKE, the stochastic superoptimizer☆64Updated 6 years ago
- The SAW core language.☆54Updated 4 years ago