Automated flaw detection in algebraic specifications

DOI10.1007/S10817-010-9166-1MaRDI QIDQ616853zbMATH OpenOpenAlexFDO

Authors 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

abstract data typesalgebraic specificationsfinite modelsfirst-order logicformal methodsSAT checkingtheorem proving

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Automating Algebraic Specifications of Non-freely Generated Data Types
• scientific article; zbMATH DE number 1765705
• Bounded Relational Analysis of Free Data Types
• scientific article; zbMATH DE number 1552508
• Automated Reasoning in Kleene Algebra

Cites work

• Algebraic Methodology and Software Technology
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Automation for interactive proof: first prototype
• Bounded Relational Analysis of Free Data Types
• CASL reference manual. The complete documentation of the common algebraic specification language.
• scientific article; zbMATH DE number 2185691 (Why is no real title available?)
• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 2006660 (Why is no real title available?)
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)
• scientific article; zbMATH DE number 1552511 (Why is no real title available?)
• scientific article; zbMATH DE number 1765705 (Why is no real title available?)
• scientific article; zbMATH DE number 1860657 (Why is no real title available?)
• scientific article; zbMATH DE number 2090301 (Why is no real title available?)
• Interactive verification of concurrent systems using symbolic execution
• Kodkod: A Relational Model Finder
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• Theorem proving in large theories
• Verifying concurrent systems with symbolic execution. Temporal reasoning is symbolic execution with a little induction.

Cited in

(6)

• How testing helps to diagnose proof failures
• Model finding for recursive functions in SMT
• Automating Algebraic Specifications of Non-freely Generated Data Types
• scientific article; zbMATH DE number 1765705 (Why is no real title available?)
• scientific article; zbMATH DE number 2090301 (Why is no real title available?)
• Bounded Relational Analysis of Free Data Types

Describes a project that uses

Uses Software

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

This page was built for publication: Automated flaw detection in algebraic specifications

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