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.