KodkodThe Kodkod Constraint Solver


Kodkod is used in a wide range of applications, including bounded verification, program synthesis, declarative execution, and specification analysis. This page lists some of the tools and theses that are based on Kodkod. For papers citing Kodkod, follow the “cited by” links on the publications page.

Tools Built on Kodkod

Alloy4 A lightweight analyzer for the Alloy modeling language.
Alloy* A general-purpose, higher-order, relational constraint solver.
aRby An embedding of Alloy in Ruby.
Nitpick A counterexample generator for Isabelle/HOL
Margrave An analyzer for security and privacy policies.
Squander A framework for unified execution of imperative and declarative code.
Rubicon A bounded verifier for Ruby on Rails applications.
MemSAT A bounded verifier for memory consistency models.
TACO A bounded verifier for Java programs annotated with JML.
Forge A bounded verifier for Java programs annotated with JFSL.
PBnJ A tool for runtime contract checking and recovery for Java programs.

Theses Using Kodkod