The Kodkod Constraint SolverApplications
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
- Allison Sullivan. Automated Testing and Sketching of Alloy Models. Ph.D. Thesis, The University Of Texas at Austin, 2017.
- Vajihollah Montaghami. Debugging Relational Declarative Models with Discriminating Examples. Ph.D. Thesis, University of Waterloo, 2017.
- Aleksandar Milicevic. Advancing Declarative Programming. Ph.D. Thesis, Massachusetts Institute of Technology, 2015.
- Divya Gopinath. Systematic Techniques for More Effective Fault Localization and Program Repair. Ph.D. Thesis, The University Of Texas at Austin, 2015.
- Razieh N. Zaeem. Contract-Driven Data Structure Repair: A Novel Approach for Error Recovery. Ph.D. Thesis, The University Of Texas at Austin, 2014.
- Jasmin C. Blanchette. Automatic Proofs and Refutations for Higher-Order Logic. Ph.D. Thesis, Technische Universität München, 2012.
- Theophilos J. Giannakopoulos. Multi-Decision Policy and Policy Combinator Specifications. M.Sc. Thesis, Worcester Polytechnic Institute, 2012.
- Juan P. Galeotti. Software Verification Using Alloy. Ph.D. Thesis, University of Buenos Aires, 2010.
- Aleksandar Milicevic. Executable Specifications for Java Programs. M.Sc. Thesis, Massachusetts Institute of Technology, 2010.
- Felix S. H. Chang. Generation of Policy-Rich Websites From Declarative Models. Ph.D. Thesis, Massachusetts Institute of Technology, 2009.
- Kuat T. Yessenov. A Lightweight Specification Language for Bounded Program Verification. M.Eng. Thesis, Massachusetts Institute of Technology, 2009.
- Greg D. Dennis. A Relational Framework for Bounded Program Verification. Ph.D. Thesis, Massachusetts Institute of Technology, 2009.
- Engin Uzuncaova. Efficient Specification-Based Testing Using Incremental Techniques. Ph.D. Thesis, University of Texas at Austin, 2008.
- Mana Taghdiri. Automating Modular Program Verification by Refining Specifications. Ph.D. Thesis, Massachusetts Institute of Technology, 2007.
- Vincent S. Yeung. Declarative Configuration Applied to Course Scheduling. M.Eng. Thesis, Massachusetts Institute of Technology, 2006.