Carini (Compositionally Arranged INductive Invariants) is a tool for inductive invariant inference in the TLA+ formal specification language. Carini is based on fully compositional inductive invariant inference, a novel technique that we are currently researching. Currently, this repository houses code for synthesizing formulaic assumptions for components of a protocol, which are then passed to Endive for inferring a local inductive invariant.
forked from cmu-soda/recomp-verify
-
Notifications
You must be signed in to change notification settings - Fork 0
This tool synthesizes symbolic assumptions for TLA+ specifications.
License
cmu-soda/carini
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
This tool synthesizes symbolic assumptions for TLA+ specifications.
Resources
License
Stars
Watchers
Forks
Releases
3D78
No releases published
Packages 0
No packages published
Languages
- Java 64.4%
- TLA 35.0%
- TeX 0.3%
- HTML 0.2%
- AspectJ 0.1%
- Shell 0.0%