Bounded Relational Analysis of Free Data Types

DOI10.1007/978-3-540-79124-9_8zbMath1138.68446OpenAlexW1517066021MaRDI QIDQ5458813

Wolfgang Reif, Gerhard Schellhorn, Andriy Dunets

Publication date: 24 April 2008

Published in: Tests and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-79124-9_8

zbMATH Keywords

verificationtheorem provingmodel checkingformal methodsabstract data typesSAT checkingFirst-order logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (2)

Automated flaw detection in algebraic specifications ⋮ Automating Algebraic Specifications of Non-freely Generated Data Types

Uses Software

• Kodkod
• KIV

Cites Work

• Automated deduction. A basis for applications. Vol. III: Applications
• Automation for interactive proof: first prototype
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• Algebraic Methodology and Software Technology
• Kodkod: A Relational Model Finder
• Tools and Algorithms for the Construction and Analysis of Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Bounded Relational Analysis of Free Data Types