`
a community of software engineering tools
all tutorial automata concurrency design encoders infrastructure languages security synthesis testing verification language
Microsoft
agl
Automatic Graph Layout
bek
A domain specific language for writing and analyzing common string functions
bex
A domain specific language for writing and analyzing string encoders and decoders
boogie
Intermediate Verification Language
chalice
A language and program verifier for reasoning about concurrent programs.
civl
Concurrent Intermediate Verification Language
code contracts
Language agnostic modular program verification and repair with abstract interpretation.
counterdog
Theorem-prover for Counterfactual Datalog
dafny
A language and program verifier for functional correctness
esm
Empirical Software Engineering and Measurement Group
fast
A domain specific language for writing and analyzing tree manipulating programs
formula
Formal Modeling Using Logic Programming and Analysis
formula2
Formal Modeling Using Logic Programming and Analysis
f*
A verification tool for higher-order stateful programs
heapdbg
Runtime heap abstraction
iz3
Efficient Interpolating Theorem Prover
koka
A function-oriented language with effect inference
pex
Automatic test generation using Dynamic Symbolic Execution for .NET
quickcode
Progamming-by-example technology for learning string transformation programs
concurrent revisions
Parallel and Concurrent Programming With Snapshots
rex
Regular Expression Exploration
seal
Side-Effects AnalysiS
spec#
A formal language for API contracts
touchdevelop
Program your phone on your phone.
vcc
A Verifier for Concurrent C
visual c++
VC++ compiler (Latest front-end build)
z3
Efficient Theorem Prover
Multicore programming Group, Imperial College London
gpuverify-cuda
A verifier for CUDA/OpenCL kernels
gpuverify-opencl
A verifier for CUDA/OpenCL kernels
NOVA-LINCS@FCT/UNL
dift
Dependent Information Flow Types: Typechecker
Otto-von-Guericke-University Magdeburg - Department of Distributed Systems
saml
Safty Analysis Modelling Language
Uppsala University
eldarica
The Model Checker