Automated reasoning for probabilistic sequential programs with theorem proving

DOI10.1007/978-3-030-88701-8_28MaRDI QIDQ2695373zbMATH OpenOpenAlexFDO

Authors Kangfeng Ye, Simon Foster, Jim 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)

Cites work

• Abstraction, Refinement and Proof for Probabilistic Systems
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 517333 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Integrated Formal Methods
• Isabelle
• Isabelle/HOL. A proof assistant for higher-order logic
• Mathematics of Program Construction
• Normal design algebra
• Probabilistic guarded commands mechanized in HOL
• Probabilistic models for the guarded command language
• Probabilistic semantics for RoboChart. A weakest completion approach
• Proofs of randomized algorithms in Coq
• The weakest prespecification

Cited in

(6)

• Bayesian ranking for strategy scheduling in automated theorem provers
• Reasoning about probabilistic sequential programs
• Reasoning about Recursive Probabilistic Programs
• Formally verified animation for RoboChart using interaction trees
• Modelling and verifying robotic software that uses neural networks
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving

Describes a project that uses

Uses Software

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

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

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