A proof assistant for Alloy specifications

DOI10.1007/978-3-642-28756-5_29MaRDI QIDQ2894289zbMATH OpenOpenAlexFDO

Authors Mattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri

Publication date 29 June 2012

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28756-5_29

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
• Bounded Relational Analysis of Free Data Types
• scientific article; zbMATH DE number 2013571
• scientific article; zbMATH DE number 1973995
• Using the Alloy analyzer to verify data refinement in Z

Cited in

(4)

• Towards a small model theorem for data independent systems in Alloy
• Bounded Relational Analysis of Free Data Types
• Relational and Kleene-Algebraic Methods in Computer Science
• Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications

Describes a project that uses

Uses Software

• Alloy
• PVS
• Kelloy
• JKelloy
• Athena
• KeY

This page was built for publication: A proof assistant for Alloy specifications

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