Unifying Theories in Isabelle/HOL

DOI10.1007/978-3-642-16690-7_9zbMath1309.68045OpenAlexW43811100MaRDI QIDQ3055747

Abderrahmane Feliachi, Burkhart Wolff, Marie-Claude Gaudel

Publication date: 9 November 2010

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

Full work available at URL: https://doi.org/10.1007/978-3-642-16690-7_9

zbMATH Keywords

theorem provingCSPIsabelle/HOLCircusUTP

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

The Logic of U ·(TP)2 ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Automated Algebraic Reasoning for Collections and Local Variables with Lenses ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ Angelic processes for CSP via the UTP ⋮ A UTP semantics for communicating processes with shared variables and its formal encoding in PVS ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• ProofPower

This page was built for publication: Unifying Theories in Isabelle/HOL