# PV2 tools in ProVerBPV2

PV2 tools generate an executable artefact from a formal one that specifies the desired properties and conditions, without necessarily providing means of explicitly verifying the correctness of the synthesised code. For instance, it could be a test data generator that produces a lot of diverse test cases from a model.- ADAC (synthesises an approximate circuit from a given one and a set of constraints)
- AIGEN (synthesises a transition system from the set of requirements)
- AMYTISS (synthesises a spec-conforming controller from a Markov decision process)
- ATHOS (computes the synchronous counterpart of an asynchronous protocol)
- ATLAS (learns abstractions and transformers from a language and a set of synthesis problems)
- autoCode4 (synthesises a reactive controller based on requirements written in the GXW subset of LTL)
- BAS (synthesises asynchronous programs based on an LTL formula)
- Cerberus (synthesises run-time monitors for enforcing authorization policies)
- Cervino (transforms first order LTL formulae to Electrum models)
- Code2Inv (generates invariants from a C or CHC program, requires an external solver)
- Concord (given a domain-specific language and specification, it synthesises a program that satisfies the specification)
- CoqQFBV (produces a satisfiability formula for a query)
- Daisy (synthesises a Scala or C program where performance of floating-point operations are optimised)
- DaPPer (synthesises probabilistic programs from relational datasets)
- DIGITS (repairs a given loop-free program from a probabilistic specification of its desired behaviour)
- Escher (synthesises a recursive program based on input-output examples)
- FACTEST (synthesises a controller for non-linear systems with reach-avoid requirements)
- fault (generates tests for a circuit)
- FGL (transforms expressions into Boolean formulae)
- FiMDP (synthesises a controller for a resource-constrained Markov Decision Process)
- Flow* (generates flowpipes for non-linear hybrid systems)
- GACAL (generates increasingly stronger invariants for an external prover)
- GDVB (given a problem and constraints, generates benchmarks)
- GLPSOL (generates an algorithm description to solve the given problem)
- Gurobi (generates an optimised algorithm to solve a known problem)
- Hampa (synthesises a replicated object that guarantees integrity, convergence and recency)
- IAM Access Analyzer (generates findings covering a given access policy)
- Isla (generates a state graph or a test case from an architecture spec)
- JitSynth (synthesises a verified just-in-time compiler for in-kernel domain-specific languages)
- LLVM2SMT (encodes a control flow graph as an SMT formula)
- LoopInvGen (transforms program's assertions into an equivalent loop invariant)
- MachSMT (decides which solver to call per instance based on pairwise ranking comparators)
- Manthan (generates a depencency function linking two arguments of a given function)
- MightyL (compiles a temporal logic formula to a timed automaton)
- MLTLconverter (given a MLTL formula, generate an equivalent in another LTL dialect to be used with an external solver)
- Mona (translates WS1S and WS2S into minimum DFAs and GTAs)
- MOVEC (performs aspect weaving)
- Mapping Synthesis Tool (given a high level spec and a low level spec, produces a set of property-preserving mappings)
- MU-CSeq (sequentialises a parallel C program)
- NIS (synthesises inductive invariants for a SyGuS problem)
- PAGAI (computes inductive invariants on the numerical variables of a given program)
- PARTY (generates an automaton from source code or spec)
- PAYNT (synthesise a full program from its sketch and desired properties)
- PBTS (compute piecewise barrier tubes configuration from a system spec)
- PCSat (generates an SMT problem from a pfwCSP spec, requires an external solver)
- PeSCo (generates the best fitting configuration for CPAchecker that fits previous experiences)
- Pithya (provide a set of parameter valuations to satisfy the given formula on a given dynamical system)
- PLearn (synthesises a program conforming to a subgrammar of a given grammar)
- POROUS (generates invariants for given affine functions)
- PoS4MPC (synthesises security policy for secure multi-party computation)
- PRISM-PSY (synthesises model parameters such that a property meets a given threshold)
- QuaSi (tries to solve a SyGuS problem with quantitative objectives)
- RealSyn (synthesises a set of controllers that meet the reach-avoid specification)
- ReVerC (transforms irreversible programs into reversible circuits)
- Rubicon (translates properties from PRISM to Dice)
- Sample (generates permission pre- and postconditions for Viper programs)
- SATzilla (decides which solver to call per instance based on predictors)
- Safety Analysis of Weakly-Hard Systems (generates several safe regions of weakly hard system)
- SceneChecker (transforms scenarios for hybrid control systems to reachability problems, requires an external solver)
- SCHMIT (synthesises a mitigation policy with the highest entropy)
- Scoot (extracts models from source code for other checkers, generates code that does not rely on SystemC)
- SGR(k) (generates two finite-state transducers to fit with a given artefact into the Adapter design pattern)
- Sketcham (synthesises a full program from its sketch)
- SMT-PGFPS (computes a minimal cut set of a hypergraph)
- Speculoos (generates AIGER circuits based on descriptions of register updates and output expressions)
- SRLBC (generates a DNN for a given grid)
- StringFuzz (generates and transforms SMT-LIB instances)
- Strix (synthesises a controller for an LTL formula)
- Synduce (generates equivalent recursive functions when migrating from one data structure to another)
- SyNET (generates configurations for routers such that given requirements are satisfied)
- SynPlexity (synthesises recursive functions that satisfy a functional specification and an asymptotic resource bound)
- SYNUDIC (synthesises a loop-free program based on a sketch of the desired program)
- syrup (generates optimized EVM bytecode to transform the source into the target stack)
- tAIlor (generates a configuration for an abstract interpreter from constraints)
- TarTar (suggests repairs based on a timed diagnostic trace)
- τ-DIGITS (fill holes a given loop-free program from a probabilistic specification of its desired behaviour)
- TFML (generates a quantifier-free formula overapproximating a given quantified formula)
- TheSy (discovers lemmas based on data types and recursive definitions)
- Typpete (infers type annotations for Python programs)
- UDDER (generates a bounded version of the given unbounded verification problem)
- v2c (translates a Register Transfer Level hardware circuit description into a C program)
- Violat (generates classes attempting to violate properties)
- Why3 (can generate correct OCaml programs or use external provers to discharge verification conditions)
- Yosys (converts from Verilog to various formats and connects to other libraries)

84 items on this list.