Publications

(2024). Formally verified animation for RoboChart using interaction trees. Journal of Logical and Algebraic Methods in Programming.

Cite DOI URL

(2023). Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment. 2023 IEEE 19th International Conference on Automation Science and Engineering (CASE).

Cite DOI

(2022). Formally Verified Animation for RoboChart Using Interaction Trees. Formal Methods and Software Engineering.

PDF Cite DOI

(2021). Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving. Relational and Algebraic Methods in Computer Science.

PDF Cite DOI

(2021). Probabilistic modelling and verification using RoboChart and PRISM. Software and Systems Modeling.

PDF DOI

(2021). RoboStar Technology: Modelling Uncertainty in RoboChart Using Probability. Software Engineering for Robotics.

PDF Cite DOI

(2021). Automated verification of reactive and concurrent programs by calculation. Journal of Logical and Algebraic Methods in Programming.

PDF Cite DOI

(2020). Automated Verification of Reactive and Concurrent Programs by Calculation. CoRR.

PDF

(2020). Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP. From Astrophysics to Unconventional Computation: Essays Presented to Susan Stepney on the Occasion of her 60th Birthday.

PDF DOI

(2019). Probabilistic Semantics for RoboChart - A Weakest Completion Approach. Unifying Theories of Programming - 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings.

PDF DOI

(2018). Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP.

PDF

(2018). Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. Relational and Algebraic Methods in Computer Science.

PDF DOI

(2018). Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. CoRR.

PDF

(2017). Model checking of state-rich formalism by linking to $$CSP,‖ ,B$$CSP‖B. International Journal on Software Tools for Technology Transfer.

PDF DOI