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) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

• 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?)
• A Theory of Pointers for the UTP
• A UTP semantics for \textsf{Circus}
• A theoretical basis for stepwise refinement and the programming calculus
• 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
• 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
• UTP semantics for Handel-C
• Unifying theories in ProofPower-Z

Cited in

(12)

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

Describes a project that uses

Uses Software

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

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)