Automating Algebraic Specifications of Non-freely Generated Data Types

DOI10.1007/978-3-540-88387-6_12zbMath1183.68368OpenAlexW1526091374MaRDI QIDQ3540070

Gerhard Schellhorn, Andriy Dunets, Wolfgang Reif

Publication date: 20 November 2008

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-88387-6_12

zbMATH Keywords

theorem provingfirst-order logicfinite modelsalgebraic specificationsabstract data typesSAT checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (1)

Automated flaw detection in algebraic specifications

Uses Software

• Isabelle
• CASL
• OTTER
• PVS
• zChaff
• Prover9
• FINDER
• Mace4
• Kodkod
• KIV

Cites Work

• Isabelle. A generic theorem prover
• CASL reference manual. The complete documentation of the common algebraic specification language.
• Automation for interactive proof: first prototype
• Algebraic Methodology and Software Technology
• Bounded Relational Analysis of Free Data Types
• Kodkod: A Relational Model Finder
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Automating Algebraic Specifications of Non-freely Generated Data Types