# PV1 tools in ProVerBPV1

PV1 tools encode the formal expectations about the artefacts that they manipulate, and report back to their users about found inconsistencies. A typical resident of this level could be a linter: a tool that analyses your program and complains about places where your program does not conform to its expectations.- AEON (analyses bifurcations of a parametrised Boolean network)
- Alive2 (formalises LLVM code and transformations and allows to analyse them)
- AliveInLean (verifies its own expectations of a given compiler optimisation)
- AMUSIC (counts minimal unsatisfiable subsets of a given formula in CNF)
- APOET (analyses a multi-threaded program to see if it conforms to expectations of the tool)
- AProVE (analyses programs for termination)
- ATLAS(2) (checks or infers types by static analysis)
- BDD4BNN (encodes a binarized neural network and input region into a BDD)
- BINSEC (framework providing abstractions for binary code analysis)
- CabPy (solves a two-player reachability game)
- Cerberus-BMC (checks a C program against a predefined concurrency model)
- Certifaiger (checks whether the result of a k-induction-based model checker is correct)
- CLEAR (checks a labelled transition system and visualises its problematic part)
- COLA (computes complementation, determinization and containment for Büchi automaton)
- ComPACT (checks termination of a given program)
- CountMUST (counts minimal unsatisfiable subsets of a given boolean formula)
- ddSMT (minimizes an input that triggers faulty behavior in an SMT solver)
- DEEPSEC (checks whether two cryptographic protocols are trace equivalent)
- DetLP (comparator of two weighted automata)
- DLV (verifies that a neural network has no misclassifications)
- dtControl (visualises a previously synthesised controller)
- Endicheck (detects endianness bugs in annotated C/C++ programs)
- EntropyEstimation (computes the Shannon entropy for a given program)
- Faial (checks data-race freedom of GPU kernels)
- FOADA (checks whether the given automaton is empty)
- FORKLIFT (checks language-inclusion for Büchi automata)
- Frama-C (framework providing abstractions for C code analysis)
- FreqTerm (checks whether the encoded program terminates)
- GANAK (Counts number of possible solutions for a Boolean formula)
- GPUDrano (detects uncoalesced memory accesses in CUDA programs)
- GRAT (checks correctness of SAT solver certificates)
- Hemiola (framework for designing protocols without inconsistent interleavings)
- HipTNT+ (analyses imperative programs for termination)
- HQSpre (simplifies quantified Boolean formulas and dependency quantified Boolean formulas)
- Hylaa (computes a set of safe reachable states for a given hybrid automaton)
- InterpChecker (checks whether unsafe states in C code can be reached)
- iRankFinder (infers ranking functions for loops)
- jcstress (executes test cases in an order that may lead to faults)
- KMC (checks compatibility of communicating automata)
- LOBER (computes lower bounds of worst-cast costs)
- Loopus (computes symbolic bounds on loops in a program)
- MeMin (minimises Mealy machines)
- MetaVal (checks whether the witness for a specific program and property is valid)
- mlir-tv (checks correctness of transformations for MLIR)
- Montre (searches for patterns of a given form in a stream of events)
- Murxla (fuzzer for SMT solvers)
- MuVal (checks whether a C program will (non-)terminate)
- µZ (computes fixed points of a set of constraints)
- nnenum (given an unsafe set an a neural network, checks whether the set overlaps with the output of the network)
- nonreach (determines whether a problem for a rewrite system is nonreachable or infeasible)
- NOPE (given a syntax-guided synthesis problem, checks whether it is realisable)
- Oink (solves a parity game)
- Origami (verifies reachability in networks in the presence of faults)
- Owl (formally manipulates LTL formulae, Büchi automata and ω-automata)
- Pastis (can compute and produce proofs for resource bounds of imperative programs)
- Peregrine (verifies that a population protocol computes a user-specified predicate)
- PEREGRiNN (checks whether an image is always classified the same when it's perturbed)
- Petit Poucet (operates with functions and their combinations formally and explainably)
- PIRK (computes reachable sets of high-dimensional non-linear systems)
- py-metric-temporal-logic (manipulates and evaluates metric temporal logic formulae)
- POET (analyses a multi-threaded program to see if it conforms to expectations of the tool)
- PrIC3 (checks if the Markov decision process is safe)
- prohver (computes safe upper bounds for probabilistic reachability probabilities)
- PROVER (runs 100 tests through a neural network, testing its noise robustness)
- PySMT (provides API for creating SMT formulae, manipulating them and converting them for different solvers to use)
- qtpi (checks that quantum programs obey real-world restrictions and simulates quantum programs)
- QuIP (comparator of two weighted automata)
- QuIPFly (comparator of two weighted automata)
- Rabinizer (can translate LTL formulae into different types of automata)
- RABIT (checks inclusion of languages generated by two Büchi automata)
- RanK (computes termination and worst case computational complexity)
- Ranker (constructs the complement of a Büchi automaton)
- RCaml (checks if a given program is type safe)
- Reduce (minimizes Büchi automata)
- RINO (Computes reachable sets for dynamical systems)
- ROLL (learns, transforms, inverts, complements Büchi automata)
- S3 (calculates the upper bound for the model count for a given formula)
- SCInfer (determines whether nodes of a cryptographic program are perfectly masked)
- Seminator (transforms a transition-based generalised Büchi automaton into an equivalent semi-deterministic one)
- SeQuaiA (handles and analyses chemical reaction networks)
- SISBMI (by solving a BMI problem checks if the unsafe state region is reachable)
- SMTCoq (imports other solvers' proof witnesses and certificates to Coq)
- SPAN (computes whether two protocols are indistinguishable)
- Spot (manipulates LTL formulae and ω-automata)
- STLInspector (aids the creation of signal temporal logic specs)
- StreamLAB (analyses input specs and reports on its memory consumption and runtime properties)
- SVPALib (supports creating and transforming symbolic automata)
- Sylvan (implements consistency-preserving transformations of BDDs on multicore)
- SyReNN (computes a symbolic representation of a neural network as linear functions)
- TChecker (can compute reachable states and detect syntax errors of timed automata)
- TcT (determines the complexity, including proof, of a given integer transition system or term rewrite system)
- Termite (computes a ranking function for a given program)
- TTT2 (produces a proof of termination for a term rewrite system)
- VeriAbs (performs several predefined analyses on C programs to make them compatible with a bounded model checker)
- VeriQFair (computes the Lipschitz constant of a quantum decision model)
- Verisig (performs reachability analysis on closed-loop systems with neural network controllers)
- z3overlay (enables type-safe creation of SMT formulae)
- Zelkova (performs one of built-in checks on an access policy)

98 items on this list.