Unifying Heterogeneous State-Spaces with Lenses

DOI10.1007/978-3-319-46750-4_17zbMath1482.68089OpenAlexW2521918545MaRDI QIDQ3179407

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

Publication date: 21 December 2016

Published in: Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL: https://eprints.whiterose.ac.uk/105106/1/lenses.pdf

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (6)

Automated Algebraic Reasoning for Collections and Local Variables with Lenses ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ Unifying theories of time with generalised reactive processes ⋮ Unifying theories of reactive design contracts ⋮ Automated verification of reactive and concurrent programs by calculation ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• ProofPower
• Sledgehammer
• Isabelle/Circus
• seL4
• Transfer
• Lifting
• Isabelle/UTP
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Building program construction and verification tools from algebraic principles
• A UTP semantics for \textsf{Circus}
• Cylindric algebras. Part II
• Isabelle/HOL. A proof assistant for higher-order logic
• Isabelle/UTP: A Mechanised Theory Engineering Framework
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Program Construction and Verification Tool for Separation Logic
• A Clear Picture of Lens Laws
• Towards a UTP Semantics for Modelica
• An Axiomatic Value Model for Isabelle/UTP
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Unifying Theories in Isabelle/HOL
• Automatic Proof and Disproof in Isabelle/HOL
• Laws of programming
• Unifying Theories in ProofPower-Z
• Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL

This page was built for publication: Unifying Heterogeneous State-Spaces with Lenses