Automated reasoning for probabilistic sequential programs with theorem proving

DOI10.1007/978-3-030-88701-8_28OpenAlexW3208322524MaRDI QIDQ2695373

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

Publication date: 30 March 2023

Full work available at URL: https://doi.org/10.1007/978-3-030-88701-8_28

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Related Items (1)

Formally verified animation for RoboChart using interaction trees

Uses Software

• Coq
• Isabelle
• ML
• Isabelle/HOL
• HOL
• pGCL
• Isabelle/UTP

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle
• Normal design algebra
• Proofs of randomized algorithms in Coq
• The weakest prespecification
• Probabilistic models for the guarded command language
• Isabelle/HOL. A proof assistant for higher-order logic
• Probabilistic semantics for RoboChart. A weakest completion approach
• Probabilistic guarded commands mechanized in HOL
• Guarded commands, nondeterminacy and formal derivation of programs
• Abstraction, Refinement and Proof for Probabilistic Systems
• Mathematics of Program Construction
• Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP
• Integrated Formal Methods

This page was built for publication: Automated reasoning for probabilistic sequential programs with theorem proving