# PV4 tools in ProVerBPV4

PV4 tools operate within a particular paradigm and derive their actions, conclusions and even properties that they need to check, from a built-in formal specification. For example, such a tool can guarantee freedom of deadlocks in a multi-threaded application, or data consistency in a database management system. Generated property set cannot be explicitly adjusted for tools of this level.- 2LS (can generate properties within certain conditions)
- adaptG2WSAT (produces a satisfiability result for a formula with lookahead and adaptive noise)
- Alt-Ergo (produces a satisfiability result for a formula)
- APRON (infers numerical properties of a program, proves the absence of errors of some classes)
- Barcelogic (produces a satisfiability result for a formula)
- BINSEC-RSE (a symbolic verifier of binary code dedicated to robust reachability)
- Bitwuzla (produces a satisfiability result for a formula)
- Boogie (infers invariants and generates verification conditions to pass to Z3)
- Boolector (produces a satisfiability result for a formula)
- BoSy (proves realisability of a given property)
- BoSyHyper (proves realizability of a given hyperproperty)
- Breach (aids property investigation in deterministic models of hybrid dynamical systems)
- BtorMC (checks safety properties of models with registers and memories)
- CADET (produces a satisfiability result for a 2QBF)
- CaDiCaL (produces a satisfiability result for a formula)
- cake_lpr (takes a proof and checks whether it satisfies linear propagation redundancy expectations)
- CAQE (produces a satisfiability result for a quantified boolean formula)
- CloudFORMAL (checks common security best-practices and user-specified queries of a cloud configuration)
- Colibri (produces a satisfiability result for a formula)
- Consensus Verifier (translates a consensus algorithm into a PROMELA model and LTL properties)
- CryptoMiniSat (produces a satisfiability result for a formula in CNF)
- CVC3 (produces a validity/satisfiability result for a formula)
- CVC4 (produces a satisfiability result for a formula)
- cvc4sy (proves unsatisfiability of a narrow class of formulae with counterexample-guided inductive synthesis)
- cvc5 (produces a satisfiability result for a formula)
- Dafny (checks user-specified annotations and languages' rules for a Dafny program)
- Dartagnan (checks assertions in a C program within a chosen memory spec)
- DepthK (checks safety properties for a C program)
- DLC (compiles a formal specification of a concurrent system to a program)
- dReal (produces a satisfiability result for a formula)
- DryVR (produces a satisfiability/reachability result for a hybrid control system)
- EAHyper (checks satisfiability, implication and equivalence of hyperproperties)
- Electrum Analyzer (checks assertions and LTL properties in Electrum models with bounded or unbounded model checking)
- ESBMC (checks safety properties in C programs, can generate invariants)
- Eureka (produces a satisfiability result for a formula with a backtrack search)
- FACT (computes confidence intervals for given properties of timed automata)
- FreqHorn (proves satisfiability of a CHC system by generating invariants)
- Glucose (produces a satisfiability result for a formula in CNF)
- gNovelty (produces a satisfiability result for a CNF formula)
- Gobra (checks memory safety, crash safety, data-race freedom, and user-provided specifications for Go programs)
- GRASShopper (checks user-specified contracts and memory safety of programs in its own language)
- GSpacer (produces a satisfiability result for a given CHC)
- IFC-BMC (checks if a program is safe with respect to variables marked secret)
- IFC-CEGAR (checks if a program is safe with respect to variables marked secret)
- JayHorn (checks user-specified assertions and infers some annotations for Java programs)
- JKind (infers invariants and checks user-specified properties for a Lustre system)
- kcnfs (produces a satisfiability result for a formula based on its backbone)
- Kissat (produces a satisfiability result for a formula)
- LCTD (generates increasingly precise tests to pinpoint an error or prove program correct)
- Lingeling (produces a satisfiability result for a formula)
- Map2Check (checks user-specified properties, overflows and memory-safety of C programs)
- march_dl (produces a satisfiability result with equivalence reasoning and double lookahead heuristics)
- march_eq (produces a satisfiability result with equivalence reasoning and lookahead heuristics)
- MathSAT (produces a satisfiability result for a formula)
- MCHyper (proves given properties on a given circuit)
- MetAcsl (checks high-level ACSL requirements by propagating them across the codebase)
- MiniSat (produces a satisfiability result for a formula)
- MiniSat+ (produces a satisfiability result for a formula)
- MoGym (verifies reach-avoid objective for trained decision-making agent)
- MonoSAT (produces a satisfiability result for a formula)
- MXC (produces a satisfiability result for a formula)
- Nagini (verifies general properties like termination and deadlock freedom of Python programs)
- NNV (checks whether the given network is safe)
- nuXmv (checks user-specified properties of a transition system, computes)
- OptiMathSAT (produces a satisfiability result and a corresponding model, for a formula)
- PAF (computers sound but tight probabilistic bounds to roundoff errors in arithmetic expressions)
- ParaFROST (produces a satisfiability result for a formula)
- PicoSAT (produces a satisfiability result for a formula)
- plingeling (produces a satisfiability result for a formula)
- PrDK (a DSL and a language workbench to create protocols as automata)
- PredatorHP (checks memory-related errors and user-specified properties in C programs)
- Q3B (produces a satisfiability result for a formula)
- QuAbS (produces a satisfiability result for a quantified boolean formula)
- Reluplex (produces a satisfiability result for a formula)
- RSat (produces a satisfiability result for a formula)
- RTD-Finder (can check deadlock-freedom and user-specified safety properties of RT-BIP models)
- Sat4j (produces a satisfiability result for a formula)
- SATenstein (produces a satisfiability result with a custom built solver)
- Scam-V (randomly generates observationally equivalent inputs and checks their equivalence)
- Symbolic Liveness Analysis (detects liveness violations)
- SMTInterpol (produces a satisfiability result for a formula)
- Spacer (produces a satisfiability result for Constrained Horn Clauses)
- SPARK (checks user-specified specifications and absence of runtime errors for Ada programs)
- SPASS-SATT (produces a satisfiability result for a formula)
- SPEAR (proves a theorem about software verification conditions, formulated in bit-vectors)
- SYCO (provides traces of deadlocks in a concurrent system)
- Symbiotic (can detect assertion violations and memory-related bugs in C programs)
- SyMon (checks whether an event log conforms to the automata specification)
- TTS (produces a satisfiability result for a proposition)
- Ultimate Automizer (checks user-specified properties and some built-in properties, e.g. memory safety, of a C program for a specified architecture)
- Ultimate Taipan (checks properties of a C program for a specified architecture and memory model)
- Unique (generates interpolant graphs from CNF formulae)
- UWrMaxSat (a complete solver for partial weighted MaxSAT instances)
- Vallst (produces a satisfiability result for a Boolean formula)
- VerCors (verifies user-written properties and memory-safety for a program)
- Verifast (checks for illegal memory accesses, data races and user-written specifications in C/Java code)
- Yices (produces a satisfiability result for a formula)
- Yogar-CBMC (converts a multi-threaded program into an event order graph and verifies its sequential consistency)
- Z3 (produces a satisfiability result for a formula)
- Z3str3RE (part of Z3, produces a satisfiability result for a set of constrains)
- zChaff (produces a satisfiability result for a formula in CNF)

101 items on this list.