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.