Publications

2020

• S. Foster, Y. Nemouchi, M. Gleirscher, R. Wei, T. Kelly. Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM. Under consideration for Formal Aspects of Computing. Preprint.
• S. Foster, K. Ye, A. Cavalcanti, J. Woodcock. Automated Verification of Reactive and Concurrent Programs by Calculation. Under consideration for Journal of Logic and Algebraic Methods for Programming. Preprint.
• S. Foster, M. Gleirscher, R. Calinescu. Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles. 25th Intl. Conf. on Engineering of Complex Computer Systems (ICECCS 2020). October 2020. Preprint.
• S. Foster, J. Baxter. Automated Algebraic Reasoning for Collections and Local Variables with Lenses. 18th Intl. Conf. on Relational and Algebraic Methods in Computer Science (RAMiCS 2020). LNCS 12062. Springer. October 2020.
• S. Foster, J. J. H. Munive, G. Struth. Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL. 18th Intl. Conf. on Relational and Algebraic Methods in Computer Science (RAMiCS 2020). LNCS 12062. Springer. October 2020.
• S. Foster, J. Baxter, A. Cavalcanti, J. Woodcock, F. Zeyda. Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP. Science of Computer Programming, volume 197. October 2020.
• S. Foster, Y. Nemouchi, C. O’Halloran, N. Tudor, K. Stephenson. Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study. Proc. 8th Intl. Conf. on Formal Methods in Software Engineering (FormaliSE 2020). ACM. October 2020.

2019

• Y. Nemouchi, S. Foster, M. Gleirscher. Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. Proc. 15th Intl. Conf. on Integrated Formal Methods (iFM 2019). LNCS 11918. December 2019.
• M. Gleirscher, S. Foster, J.Woodcock. New Opportunities for Integrated Formal Methods. ACM Computing Surveys, October 2019.
• S. Foster. Hybrid Relations in Isabelle/UTP. In Proc. 7th Intl. Symp. on Unifying Theories of Programming (UTP 2019). LNCS 11885. October 2019.
• S. Foster, A. Cavalcanti, S. Canham, J. Woodcock, F. Zeyda. Unifying theories of reactive design contracts. Theoretical Computer Science journal, volume 802. September 2019.
• J. Woodcock, A. Cavalcanti, S. Foster, A. Mota, K. Ye. Probabilistic Semantics for RoboChart: A Weakest Completion Approach. In Proc. 7th Intl. Symp. on Unifying Theories of Programming (UTP 2019). LNCS 11885. October 2019.
• M. Gleirscher, S. Foster, and Y. Nemouchi. Evolution of Formal Model Based Assurance Cases for Autonomous Robots. Proc. 17th Intl. Conf. on Software Engineering and Formal Methods (SEFM 2019). September 2019.
• S. Foster, F. Zeyda, et al. Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming. Archive of Formal Proofs (AFP). Frebruary 2019.

2018

• S. Foster, J. Baxter, A. Cavalcanti, A. Miyazawa, J. Woodcock. Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. FACS 2018. LNCS 11222. Preprint
• S. Foster, K. Ye, A. Cavalcanti, J. Woodcock. Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. RAMiCS 2018. LNCS 11194. Preprint.
• S. Foster, A. Cavalcanti, J. Woodcock, F. Zeyda. Unifying Theories of Time with Generalised Reactive Processes. Information Processing Letters. Volume 135. July 2018. Preprint.