Karp-Miller
Petri net coverability checker
An algorithm to decide coverability in Petri nets using the Karp-Miller tree construction
A Coq mechanization of the Karp-Miller algorithm based on Kruskal-AlmostFull
1 stars
2 watching
0 forks
Language: Coq
last commit: 8 months ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| dmxlarchey/kruskal-finite | Tools for proving properties about finite types and predicates using proof assistants | 0 |
| dmxlarchey/coq-kruskal | A comprehensive library of constructive Coq proofs for Kruskal's tree theorem and related concepts. | 0 |
| dmxlarchey/kruskal-trees | Formalizes rose trees in Coq with implementations of induction principles and manipulation tools | 1 |
 mciepluc/cocotb-coverage | Tools for enhanced verification of digital circuits | 104 |
| dmxlarchey/kruskal-higman | Provides detailed proofs and tools for Higman's theorem on unary trees | 0 |
| dmxlarchey/kruskal-veldman | A detailed proof of Wim Veldman's tree theorem adaptation in Coq | 0 |
 rasta-mouse/ppenum | A tool to determine the protection level of a process using a simple Binary Object Formatter (BOF) approach. | 104 |
 stanford-centaur/pono | A flexible and extensible SMT-based model checker that verifies the correctness of systems | 81 |
| dmxlarchey/kruskal-theorems | A library that provides formal proofs of tree theorems using inductive type theory. | 1 |
 oyam/pytorch-dpns | PyTorch implementation of a deep learning model for image segmentation | 90 |
| dmxlarchey/relevant-decidability | Mechanization of a proof for the decidability of Implicational Relevance Logic | 0 |
 aantron/bisect_ppx | An open-source tool for generating code coverage reports for OCaml and ReScript projects | 302 |
 kgpml/hyperspectral | Developing Deep Learning models for classifying land covers in hyperspectral images using Neural Networks | 298 |
| dmxlarchey/quasi-morphisms | A Coq library providing tools and definitions for quasi-morphisms in the context of Almost Full relations | 1 |
| dmxlarchey/kruskal-fan | A Coq implementation of the Fan theorem and König's lemma for proving properties about monotone relations on lists and finite fans. | 1 |