CompoSAT: specification-guided coverage for model finding

DOI10.1007/978-3-319-95582-7_34zbMath1460.68064OpenAlexW2809205514MaRDI QIDQ2024373

Tim Nelson, Sorawee Porncharoenwase, Shriram Krishnamurthi

Publication date: 4 May 2021

Full work available at URL: https://doi.org/10.1007/978-3-319-95582-7_34

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

CompoSAT, Pardinus: a temporal relational model finder

Uses Software

• CUTE
• MiniSat
• Alloy
• z3
• Mace4
• Kodkod
• TestEra
• Korat
• Alloy*
• margrave
• CD2Alloy
• cddiff
• Bordeaux
• Whispec
• VERMEER
• WhyLine

Cites Work

• Unnamed Item
• Unnamed Item
• Elements of finite model theory.
• Alloy*: a general-purpose higher-order relational constraint solver
• Generating effective symmetry-breaking predicates for search problems
• Exploring Theories with a Model-Finding Assistant
• Systematic mistake analysis of digital computer programs
• Symbolic execution and program testing
• Theory and Applications of Satisfiability Testing
• Searching for Shapes in Cryptographic Protocols
• Kodkod: A Relational Model Finder