Unifying theories of programming in Isabelle

DOI10.1007/978-3-642-39721-9_3MaRDI QIDQ2948230zbMATH OpenOpenAlexFDO

Authors Simon Foster, Jim Woodcock

Publication date 30 September 2015

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

Full work available at URL https://eprints.whiterose.ac.uk/94531/1/utp_in_isabelle.pdf

zbMATH Keywords

denotational semanticsinteractive theorem provingIsabellelaws of programmingunifying theories of programming (UTP)

Mathematics Subject Classification ID

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

Recommendations

• Unifying theories in Isabelle/HOL
• Isabelle/UTP: a mechanised theory engineering framework
• Integrated Formal Methods
• Unifying theories in ProofPower-Z
• Mechanical reasoning about families of UTP theories

Cites work

• A theoretical basis for stepwise refinement and the programming calculus
• A Theory of Pointers for the UTP
• A UTP semantics for \textsf{Circus}
• Automatic proof and disproof in Isabelle/HOL
• Circus Time with Reactive Designs
• Component publications and compositions
• Generating denotational semantics from algebraic semantics for event-driven system-level language
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 3936465 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1949640 (Why is no real title available?)
• scientific article; zbMATH DE number 2080001 (Why is no real title available?)
• scientific article; zbMATH DE number 2090152 (Why is no real title available?)
• Integrated Formal Methods
• Mathematics of Program Construction
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Refinement Calculus
• Retrospective and Prospective for Unifying Theories of Programming
• The B-Book
• Unifying theories in ProofPower-Z
• UTP semantics for Handel-C

Cited in

(12)

• Towards verification of cyber-physical systems with UTP and Isabelle/HOL
• A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
• Unifying theories in ProofPower-Z
• Isabelle/UTP: a mechanised theory engineering framework
• Comprehending Isabelle/HOL’s Consistency
• Unifying theories in Isabelle/HOL
• The Isabelle Framework
• Theories of programming. The life and works of Tony Hoare
• Unifying Theories in ProofPower-Z
• A Mechanized Model of the Theory of Objects
• Mechanizing UNITY in Isabelle
• Integrated Formal Methods

Describes a project that uses

Uses Software

• Isabelle
• Handel-C
• Isabelle/Circus
• Waldmeister
• Sledgehammer
• SPASS
• Z
• VAMPIRE
• Nitpick
• Isabelle/HOL
• z3
• ProofPower
• Circus

This page was built for publication: Unifying theories of programming in Isabelle

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