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, papers, and theses that are based on Kodkod.

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.
Rosette
A language for building tools for program synthesis, verification, and more.
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.
MemSAT
A bounded verifier for memory consistency models.
Rubicon
A bounded verifier for Ruby on Rails applications.
PBnJ
A tool for runtime contract checking and recovery for Java programs.
TACO
A bounded verifier for Java programs annotated with JML.
Forge
A bounded verifier for Java programs annotated with JFSL.

conference & journal papers using kodkod

Alloy*: A General-Purpose Higher-Order Relational Constraint Solver
A. Milicevic, J. Near, E. Kang, and D. Jackson.
ICSE, 2015.
Static Differential Program Analysis for Software-Defined Networks
T. Nelson, A. D. Ferguson, and S. Krishnamurthi.
Formal Methods, 2015.
aRby: An Embedding of Alloy in Ruby
A. Milicevic, E. Ido, and D. Jackson.
ABZ, 2014.
Dynamite: A tool for the verification of alloy models based on PVS
M. Moscato, C. Lopez Pombo, and M. Frias.
ACM Trans. Softw. Eng. Methodol., 2014.
Target Oriented Relational Model Finding
A. Cunha, N. Macedo, and T. Guimaraes.
FASE, 2014.
Ranger: parallel analysis of Alloy models by range partitioning
N. Rosner, J. H. Siddiqui, N. Aguirre, S. Khurshid, and M. Frias.
ASE, 2013.
Rubicon: bounded verification of web applications
J. Near and D. Jackson.
FSE, 2012.
Modeling the supervisory control theory with Alloy
B. Fraikin and M. Frappier and R. St-Denis.
Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z, 2012.
Improving the effectiveness of spectra-based fault localization using specifications
D. Gopinath and R. N. Zaeem and S. Khurshid.
Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, 2012.
Optimizing MiniSAT variable orderings for the relational model finder Kodkod
M. Iser and M. Taghdiri and C. Sinz.
Proceedings of the 15th international conference on Theory and Applications of Satisfiability Testing, 2012.
Strengthening SAT-based validation of UML/OCL models by representing collections as relations
M. Kuhlmann and M. Gogolla.
Proceedings of the 8th European conference on Modelling Foundations and Applications, 2012.
Preventing arithmetic overflows in Alloy
A. Milicevic and D. Jackson.
Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z, 2012.
Extending Alloy with partial instances
V. Montaghami and D. Rayside.
Proceedings of the Third international conference on Abstract State Machines, Alloy, B, VDM, and Z, 2012.
History-Aware data structure repair using SAT
R. Nokhbeh Zaeem and D. Gopinath and S. Khurshid and K. S. McKinley.
Proceedings of the 18th international conference on Tools and Algorithms for the Construction and Analysis of Systems, 2012.
Validating B, Z and TLA+ Using ProB and Kodkod
D. Plagge and M. Leuschel.
FM'12, 2012.
Pairwise testing for software product lines: comparison of two approaches
G. Perrouin, S. Oster, S. Sen, J. Klein, B. Baudry and Y. le Traon.
Software Quality Journal, 2011.
Data refinement based testing
D. Faitelson and S. Tyszberowicz.
International Journal of Systems Assurance Engineering and Management, 2011.
A SAT-Based Approach for the Construction of Reusable Control System Components
D. Côté, B. Fraikin, M. Frappier and R. St-Denis.
Formal Methods for Industrial Critical Systems, 2011.
Automatic proof and disproof in Isabelle/HOL
J. C. Blanchette, L. Bulwahn and T. Nipkow.
8th International Symposium Frontiers of Combining Systems (FroCoS'11), 2011.
A dataflow analysis to improve SAT-based program verification
B. C. Parrino, J. P. Galeotti, D. Garbervetsky and M. Frias.
Software Engineering and Formal Methods (SEFM'11), 2011.
Extensive Validation of OCL Models by Integrating SAT Solving into {USE
M. Kuhlmann, L. Hamann and M. Gogolla.
TOOLS (49), 2011.
Specification-Based Program Repair Using SAT
D. Gopinath, M. Z. Malik and S. Khurshid.
17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), 2011.
Behavior Model Based Component Search: An Initial Assessment
C. Ghezzi and A. Mocci.
ICSE Workshop on Search-Driven Development: Users, Infrastructure, Tools and Evaluation (SUITE'10), 2010.
Dynamite 2.0: New Features Based on Unsat-Core Extraction to Improve Verification of Software Requirements
M. M. Moscato, C. G. L. Pombo and M. F. Frias.
7th International Conference on Theoretical Aspects of Computing (ICTAC'10), 2010.
Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models
J. C. Blanchette and K. Claessen.
17th international conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10), 2010.
Optimizing Incremental Scope-Bounded Checking with Data-Flow Analysis.
D. Shao, D. Gopinath, S. Khurshid and D. E. Perry.
21st International Symposium on Software Reliability Engineering (ISSRE'10), 2010.
The Margrave Tool for Firewall Analysis
T. Nelson, C. Barratt, D. J. Dougherty, K. Fisler and S. Krishnamurthi.
24th International Conference on Large Installation System Administration (LISA'10), 2010.
Alloy+HotCore: A Fast Approximation to Unsat Core
N. Dippolito, M. Frias, J. Galeotti, E. Lanzarotti and S. Mera.
Abstract State Machines, Alloy, B and Z (ABZ'10), 2010.
Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions
J. C. Blanchette.
4th International Conference on Tests and Proofs (TAP'10), 2010.
Towards Model Validation and Verification with SAT Techniques
M. Gogolla.
Algorithms and Applications for Next Generation SAT Solvers (Dagstuhl Seminar Proceedings), 2010.
Network Configuration Validation
S. Narain, R. Talpade and G. Levin.
Guide to Reliable Internet Services and Applications (1st Edition), 2010.
Monotonicity Inference for Higher-Order Formulas
J. C. Blanchette and A. Krauss.
International Joint Conference on Automated Reasoning (IJCAR'10), 2010.
Contract-Based Data Structure Repair Using Alloy
R. Nokhbeh Zaeem and S. Khurshid.
24th European Conference on Object-Oriented Programming (ECOOP'10), 2010.
Analysis of Invariants for Efficient Bounded Verification
J. P. Galeotti, N. Rosner, C. G. L. Pombo and M. F. Frias.
2010 International Symposium on Software Testing and Analysis (ISSTA'10), 2010.
Incremental Test Generation for Software Product Lines
E. Uzuncaova, S. Khurshid and D. Batory.
IEEE Transactions on Software Engineering, Vol. 36, No. 3, 2010.
MemSAT: Checking Axiomatic Specifications of Memory Models
E. Torlak, M. Vaziri and J. Dolby.
Programming Language Design and Implementation (PLDI'10), 2010.
Using Macromodels to Manage Collections of Related Models
R. Salay, J. Mylopoulos and S. Easterbrook.
21st International Conference on Advanced Information Systems Engineering (CAiSE'09), 2009.
On the Construction and Verification of Self-modifying Access Control Policies
D. Power, M. Slaymaker and A. Simpson.
6th VLDB Workshop on Secure Data Management (SDM'09), 2009.
A Spreadsheet-Like User Interface for Combinatorial Multi-Objective Optimization
D. Rayside and H. C. Estler.
Conference of the Center for Advanced Studies on Collaborative Research (CASCON'09), 2009.
An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method
D. Shao, S. Khurshid and D. Perry.
2nd World Congress on Formal Methods (FM'09), 2009.
Automated Property Verification for Large Scale B Models
M. Leuschel, J. Falampin, F. Fritz and D. Plagge.
2nd World Congress on Formal Methods (FM'09), 2009.
A Universal Self-Organization Mechanism for Role-Based Organic Computing Systems
F. Nafz, F. Ortmeier, H. Seebach, J. P. Steghöfer and W. Reif.
6th International Conference on Autonomic and Trusted Computing (ATC'09), 2009.
SAL, Kodkod, and BDDs for Validation of B Models
D. Plagge, M. Leuschel, I. Lopatkin, A. Iliasov and A. Romanovsky.
4th Workshop on Automated Formal Methods (AFM'09), 2009.
Automated Flaw Detection in Algebraic Specifications
A. Dunets, G. Schellhorn and W. Reif.
Journal of Automated Reasoning, Vol. 45, No. 4, 2009.
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
J. C. Blanchette and T. Nipkow.
3rd International Conference on Tests and Proofs (TAP'09), 2009.
Declarative Infrastructure Configuration Synthesis and Debugging
S. Narain, G. Levin, S. Malik and V. Kaul.
Journal of Network and Systems Management, Vol. 16, No. 3, 2008.
Executing Underspecified OCL Operation Contracts with a SAT Solver
M. P. Krieger and A. Knapp.
8th International Workshop on OCL Concepts and Tools (OCL'08), 2008.
Query-Aware Test Generation Using a Relational Constraint Solver
S. A. Khalek, B. Elkarablieh, Y. O. Laleye and S. Khurshid.
23rd International Conference on Automated Software Engineering (ASE'08), 2008.
Constraint Prioritization for Efficient Analysis of Declarative Models
E. Uzuncaova and S. Khurshid.
15th International Symposium on Formal Methods (FM'08), 2008.
Testing Software Product Lines Using Incremental Test Generation
E. Uzuncaova, D. Garcia, S. Khurshid and D. Batory.
19th International Symposium on Software Reliability Engineering (ISSRE'08), 2008.
Bounded Verification of Voting Software
G. Dennis, K. Yessenov and D. Jackson.
Verified Software: Theories, Tools, Experiments (VSTTE'08), 2008.
Whispec: White-Box Testing of Libraries Using Declarative Specifications
D. Shao, S. Khurshid and D. E. Perry.
Symposium on Library-Centric Software Design (LCSD'07), 2007.
A Specification-Based Approach to Testing Software Product Lines
E. Uzuncaova, D. Garcia, S. Khurshid and D. Batory.
6th International Symposium on the Foundations of Software Engineering (FSE'07), 2007.
Finding Bugs Efficiently with a SAT Solver
J. Dolby, M. Vaziri and F. Tip.
6th International Symposium on the Foundations of Software Engineering (FSE'07), 2007.
Kato: A Program Slicing Tool for Declarative Specifications
E. Uzuncaova and S. Khurshid.
29th International Conference on Software Engineering (ICSE'07), 2007.
Modular Verification of Code with SAT
G. Dennis, F. S. H. Chang and D. Jackson.
International Symposium on Software Testing and Analysis (ISSTA'06), 2006.

theses using kodkod

Contract-Driven Data Structure Repair: A Novel Approach for Error Recovery
Razieh Nokhbeh Zaeem.
Ph.D. Thesis, The University Of Texas at Austin, 2014.
Automatic Proofs and Refutations for Higher-Order Logic
J. C. Blanchette.
Ph.D. Thesis, Technische Universität München, 2012.
Multi-Decision Policy and Policy Combinator Specifications
T. J. Giannakopoulos.
M.Sc. Thesis, Worcester Polytechnic Institute, 2012.
Software Verification Using Alloy
J. P. Galeotti.
Ph.D. Thesis, University of Buenos Aires, 2010.
Executable Specifications for Java Programs
A. Milicevic.
M.Sc. Thesis, Massachusetts Institute of Technology, 2010.
Generation of Policy-Rich Websites From Declarative Models
F. S. H. Chang.
Ph.D. Thesis, Massachusetts Institute of Technology, 2009.
A Lightweight Specification Language for Bounded Program Verification
K. T. Yessenov.
M.Eng. Thesis, Massachusetts Institute of Technology, 2009.
A Relational Framework for Bounded Program Verification
G. D. Dennis.
Ph.D. Thesis, Massachusetts Institute of Technology, 2009.
Efficient Specification-Based Testing Using Incremental Techniques
E. Uzuncaova.
Ph.D. Thesis, University of Texas at Austin, 2008.
Automating Modular Program Verification by Refining Specifications
M. Taghdiri.
Ph.D. Thesis, Massachusetts Institute of Technology, 2007.
Declarative Configuration Applied to Course Scheduling
V. S. Yeung.
M.Eng. Thesis, Massachusetts Institute of Technology, 2006.