Isabelle/UTP: A Mechanised Theory Engineering Framework

DOI10.1007/978-3-319-14806-9_2zbMath1457.68061OpenAlexW1164721860MaRDI QIDQ2814613

Frank Zeyda, Simon Foster, J. C. P. Woodcock

Publication date: 22 June 2016

Published in: Unifying Theories of Programming (Search for Journal in Brave)

Full work available at URL: https://eprints.whiterose.ac.uk/174615/1/foster_utp2014.pdf

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (15)

Behavioural Models for FMI Co-simulations ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Designing a semantic model for a wide-spectrum language with concurrency ⋮ Automated Algebraic Reasoning for Collections and Local Variables with Lenses ⋮ A Unary Semigroup Trace Algebra ⋮ Translation of CCS into CSP, correct up to strong bisimulation ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Towards a UTP Semantics for Modelica ⋮ A Stepwise Approach to Linking Theories ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ UTPCalc — A Calculator for UTP Predicates ⋮ Angelic processes for CSP via the UTP ⋮ Unifying theories of reactive design contracts ⋮ Isabelle/UTP ⋮ Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Normal design algebra
• A UTP semantics for \textsf{Circus}
• Isabelle/HOL. A proof assistant for higher-order logic
• The safety-critical Java memory model formalised
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Unifying Theories of Programming in Isabelle
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Saoithín: A Theorem Prover for UTP
• Unifying Theories in Isabelle/HOL
• Formalising foundations of mathematics
• Automatic Proof and Disproof in Isabelle/HOL
• The Logic of U ·(TP)2
• UTP Semantics for Handel-C
• Mechanical Reasoning about Families of UTP Theories
• Unifying Theories in ProofPower-Z
• Automated Deduction – CADE-20

This page was built for publication: Isabelle/UTP: A Mechanised Theory Engineering Framework