Bounded Relational Analysis of Free Data Types

DOI10.1007/978-3-540-79124-9_8MaRDI QIDQ5458813zbMATH OpenOpenAlexFDO

Authors Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif

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

abstract data typesFirst-order logicformal methodsmodel checkingSAT checkingtheorem provingverification

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)

Recommendations

• Automating Algebraic Specifications of Non-freely Generated Data Types
• A proof assistant for Alloy specifications
• Automated flaw detection in algebraic specifications
• Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
• Towards a small model theorem for data independent systems in Alloy

Cites work

• Algebraic Methodology and Software Technology
• 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
• scientific article; zbMATH DE number 2185691 (Why is no real title available?)
• scientific article; zbMATH DE number 1552511 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1765705 (Why is no real title available?)
• Kodkod: A Relational Model Finder
• Tools and Algorithms for the Construction and Analysis of Systems
• Towards a small model theorem for data independent systems in Alloy
• Verifying concurrent systems with symbolic execution. Temporal reasoning is symbolic execution with a little induction.

Cited in

(4)

• Towards a small model theorem for data independent systems in Alloy
• A proof assistant for Alloy specifications
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Automated flaw detection in algebraic specifications

Describes a project that uses

Uses Software

• Kodkod
• KIV

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

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