Software

Trustfull-funded researchers have developed or contributed to the following software:

  • Algorand Verification
    • Verified model of the Algorand consensus protocol in Coq
  • Coq
    • Proof assistant and formal language for executable algorithms and theorems
  • Chip
    • Verified change impact analysis Coq library and OCaml-based tool
  • DepClean
    • Tool for automatically removing unused dependencies from Java projects
  • Giskard verification
    • Verified model of the Giskard consensus protocol in Coq
  • Hydras & Co.
    • Collaborative, documented library of discrete mathematics for Coq
  • HolBA
    • Binary analysis library for the HOL4 proof assistant
  • HOL4P4
    • Formalization in the HOL4 theorem prover of the P4 language for programming network devices.
  • mCoq
    • Mutation analysis tool for Coq verification projects
  • MIL
    • Formalization and tools in the HOL4 theorem prover of a machine independent language for defining the semantics of microarchitectural features such as out-of-order execution.
  • OpenMZ
    • Security kernel for embedded RISC-V applications
  • Ott
    • Tool for writing definitions of programming languages and calculi that can be translated to Coq and HOL4
  • Repairnator
    • Software development bot that automatically repairs build failures on continuous integration
  • Roosterize
    • Tool for suggesting lemma names in Coq verification projects
  • Scam-V
    • Abstract side channel model validation framework
  • SequenceR
    • seq2seq system to do bug fixes in source code change at the line level
  • SerAPI
    • Library and tools for (de)serialization of Coq code to and from JSON and S-expressions
  • Slumps
    • Research project on superoptimization, diversification (CROW) for WebAssembly WASM
  • Sorald
    • An automatic repair system for bug and vulnerability warnings in Java
  • Spoon
    • Metaprogramming library to analyze and transform Java source code, supporting Java 9, 10, and 11
  • Tarjan and Kosaraju
    • Verified implementation in Coq of topological sorting with extended guarantees for acyclic graphs
  • Templates for Coq projects
    • Template files for use in generating configuration files for Coq
  • VLSM
    • Formalized model in Coq for stating and solving distributed consensus problems
  • VRepair
    • AI system for for repairing vulnerabilities in C
  • Wasm-mutate
    • a new tool for fuzzing Wasm compilers, runtimes, validators, and other Wasm-consuming programs
  • xPerturb
    • Perturbation analysis, correctness attraction and randomization