Using theory morphisms for implementing formal methods tools

DOI10.1007/3-540-39185-1_4MaRDI QIDQ4435460zbMATH OpenFDO

Authors Achim D. Brucker, Burkhart Wolff

Publication date 12 November 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2646/26460059.htm

zbMATH Keywords

Formal MethodsFormal SemanticsOCLShallow EmbeddingsTheorem Proving

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Constructing specification morphisms
• Generic tools via general refinement
• Lax theory morphisms
• Structured formal development in Isabelle
• Boosting the reuse of formal specifications

Cited in

(5)

• Boosting the reuse of formal specifications
• Automatically finding theory morphisms for knowledge management
• Version and configuration management of formal theories
• Theories, implementations, and transformations
• Lax theory morphisms

Describes a project that uses

Uses Software

• DOVE
• Automath
• Coq
• Isabelle/HOL
• Nuprl
• KIV

This page was built for publication: Using theory morphisms for implementing formal methods tools

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