PV0 tools in ProVerBPV0

PV0 tools manipulate given and produced software artefacts with some degree of rigour. Conceptually such artefacts then may correspond to mathematical and formal entities, but this correspondence is mostly a matter of expectations. This category should be reasonably unpopulated since we mostly avoid to include such tools listed on this website.

• ANTLR (works with grammars which are relatively strictly structured)
• Apfloat (operates on extreme-precision real numbers (with millions of digits))
• Automata (a library to compose symbolic automata and prepare them for analysis)
• Ceramist (Coq library for reasoning about Approximate Membership Query structures)
• Crab (a library for building abstract interpretation-based analyses)
• CUDD (a C package for manipulating decision diagrams)
• DG (a library that provides data structures and algorithms for program analysis and slicing)
• EMTST (proof assistant library for reasoning about session types)
• EXIST
• FRET
• JavaSMT (API for accessing SMT solvers in Java)
• JConstraints (a Java library for working with logic constraints)
• LearnLib (a library for active automata learning)
• LEGION
• LEVEL-UP
• MPFR (C library for multiple-precision floating-point computations)
• Prosa (a repository of definitions and proofs for real-time schedulability analysis)
• SLURF
• Smt-Switch (a collection of abstract classes useful for SMT solving)
• SolCMC
• SpeAR
• SRM (quickly generates matches from regular expressions)
• UCLID5
• UDBM (library to manipulate difference bounded matrices in UPPAAL)

24 items on this list.