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: about 2 months ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| dmxlarchey/kruskal-finite | Tools for determining and working with finite data structures in a proof assistant. | 0 |
| dmxlarchey/coq-kruskal | A comprehensive library of constructive Coq proofs for Kruskal's tree theorem and related concepts. | 0 |
| dmxlarchey/kruskal-trees | A Coq library formalizing rose trees for mathematical proof and theorem proving | 1 |
 mciepluc/cocotb-coverage | Tools for enhanced verification of digital circuits | 106 |
| dmxlarchey/kruskal-higman | An inductive proof of Higman's theorem for unary trees and lists, providing a constructive basis for Kruskal's theorem | 0 |
| dmxlarchey/kruskal-veldman | Provides a constructive account of Wim Veldman's proof of a variant of Kruskal's tree theorem for rose trees in Coq. | 0 |
 rasta-mouse/ppenum | A tool to determine the protection level of a process using a simple Binary Object Formatter (BOF) approach. | 111 |
 stanford-centaur/pono | A flexible and extensible SMT-based model checker that verifies the correctness of systems | 82 |
| dmxlarchey/kruskal-theorems | Provides theorem results for tree embeddings in 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 OCaml-based tool for generating code coverage reports | 301 |
 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 proof framework for Fan theorem and König's lemma | 1 |