Automated flaw detection in algebraic specifications

DOI10.1007/s10817-010-9166-1zbMath1207.68337OpenAlexW2070717690MaRDI QIDQ616853

Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif

Publication date: 12 January 2011

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-010-9166-1

zbMATH Keywords

theorem provingfirst-order logicfinite modelsalgebraic specificationsformal methodsabstract data typesSAT checking

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

Model Finding for Recursive Functions in SMT

Uses Software

• Isabelle
• CASL
• PVS
• Prover9
• FINDER
• Mace4
• Chaff
• Kodkod
• KIV

Cites Work

• CASL reference manual. The complete documentation of the common algebraic specification language.
• Automation for interactive proof: first prototype
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Interactive verification of concurrent systems using symbolic execution
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item