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.