Formally verified animation for RoboChart using interaction trees

DOI10.1016/j.jlamp.2023.100940arXiv2303.09106MaRDI QIDQ6151624

J. C. P. Woodcock, Simon Foster, Kangfeng Ye

Publication date: 12 February 2024

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2303.09106

zbMATH Keywords

operational semanticstheorem provingCSPcode generationinteraction treesanimation of robot software

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An overview of the K semantic framework
• The weakest prespecification
• Higher-order rewrite systems and their confluence
• Probabilistic semantics for RoboChart. A weakest completion approach
• Automated reasoning for probabilistic sequential programs with theorem proving
• A Theory of Communicating Sequential Processes
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Types for Proofs and Programs

This page was built for publication: Formally verified animation for RoboChart using interaction trees