Kodkod: A Relational Model Finder

DOI10.1007/978-3-540-71209-1_49MaRDI QIDQ5758136zbMATHOpenAlexFDO

Authors Emina Torlak, Daniel Jackson

Publication date 3 September 2007

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71209-1_49

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Pardinus: a temporal relational model finder
• Reducing symmetries to generate easier SAT instances
• Satisfiability modulo bounded checking
• Finite model finding using the logic of equality with uninterpreted functions
• Relational constraint solving in SMT

Cited in

(21)

• On local domain symmetry for model expansion
• Monotonicity inference for higher-order formulas
• Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA
• From LCF to Isabelle/HOL
• Monotonicity inference for higher-order formulas
• CompoSAT: specification-guided coverage for model finding
• Specification-based program repair using SAT
• Bounded Relational Analysis of Free Data Types
• Automated flaw detection in algebraic specifications
• Automatic proof and disproof in Isabelle/HOL
• Kodkod
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Pardinus: a temporal relational model finder
• Recognition of Nested Gates in CNF Formulas
• Exploring theories with a model-finding assistant
• Handling transitive relations in first-order automated reasoning
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Alloy*: a general-purpose higher-order relational constraint solver
• A study of symmetry breaking predicates and model counting
• Model finding for recursive functions in SMT
• Constraint solving for finite model finding in SMT solvers

This page was built for publication: Kodkod: A Relational Model Finder

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5758136)