Calculational verification of reactive programs with reactive relations and Kleene algebra

DOI10.1007/978-3-030-02149-8_13MaRDI QIDQ1617824zbMATH OpenOpenAlexFDO

Authors Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock

Publication date 8 November 2018

Full work available at URL https://arxiv.org/abs/1806.02101, https://eprints.whiterose.ac.uk/134042/1/RAMICS2018.pdf

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Automated verification of reactive and concurrent programs by calculation
• A calculational approach to reactive systems
• Towards a design calculus for CSP
• Building program construction and verification tools from algebraic principles
• Program analysis and verification based on Kleene algebra in Isabelle/HOL

Cited in

(3)

• Hybrid verifications of reactive programs
• Automated verification of reactive and concurrent programs by calculation
• Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming

This page was built for publication: Calculational verification of reactive programs with reactive relations and Kleene algebra

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