Partial lists of my publications can also be found on DBLP and Google Scholar. My PhD thesis is also available here.

2022

• K. Ye, A. Cavalcanti, S. Foster, A. Miyazawa, J. Woodcock. Probabilistic modelling and verification using RoboChart and PRISM. Software and Systems Modeling, Volume 21.
• K. Ye, S. Foster, J. Woodcock. Formally Verified Animation for RoboChart Using Interaction Trees. 23rd International Conference on Engineering Formal Methods (ICFEM 2022).
• F. Yan, S. Foster, I. Habli, R. Wei. Model-based Generation of Hazard-driven Arguments and Formal Verification Evidence for Assurance Cases. 10th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2022).

2021

• K. Ye, S. Foster, J. Woodcock. Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving. 19th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2021)
• S. Foster, C.-K. Hur, J. Woodcock. Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. 32nd International Conference on Concurrency Theory (CONCUR 2021).
• S. Foster, J. J. Huerta y Munive, M. Gleirscher, G. Struth. Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. 24 International Symposium on Formal Methods (FM 2021).
• S. Foster, Y. Nemouchi, M. Gleirscher, R. Wei, T. Kelly. Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM. Formal Aspects of Computing. Preprint.
• S. Foster, K. Ye, A. Cavalcanti, J. Woodcock. Automated Verification of Reactive and Concurrent Programs by Calculation. Journal of Logic and Algebraic Methods for Programming. Preprint.

2020

• 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.

2017

• F. Zeyda, J. Ouy, S. Foster, and A. Cavalcanti. Formalised Cosimulation Models. 1st Workshop on Formal Co-simulation of Cyber-Physical Systems (CoSim-CPS). 2017. LNCS 10729.
• S. Foster and F. Zeyda. Optics in Isabelle/HOL. Archive of Formal Proofs. 2017.
• S. Foster and J. Woodcock. Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL. Concurrency, Security, and Puzzles. 2017. LNCS 10160.

2016

• S. Foster, F. Zeyda, and J. Woodcock: Unifying Heterogeneous State-Spaces with Lenses. Proc. 13th Intl. Colloq. on Theoretical Aspects of Computing (ICTAC). October 2016. LNCS 9965.
• P. G. Larsen, J. Fitzgerald, J. Woodcock, R. Nilsson, C. Gamble, S. Foster: Towards Semantically Integrated Models and Tools for Cyber-Physical Systems Design. Proc. 7th Intl. Symp. on Leveraging Applications of Formal Methods (ISoLA). 2016. LNCS 9952
• J. Woodcock, S. Foster, and A. Butterfield: Heterogeneous Semantics and Unifying Theories. Proc. 7th Intl. Symp. on Leveraging Applications of Formal Methods (ISoLA). 2016. LNCS 9952
• J. Woodcock and S. Foster: UTP by Example: Designs. 2nd Intl. School on Engineering Trustworthy Software Systems (SETSS). 2016. LNCS 10215
• S. Foster, B. Thiele, A. Cavalcanti, and J. Woodcock: Towards a UTP Semantics for Modelica. Proc. 6th Intl. Symp. on Unifying Theories of Programming (UTP). 2016. LNCS 10134
• F. Zeyda, S. Foster, and L. Freitas: An Axiomatic Value Model for Isabelle/UTP. Proc. 6th Intl. Symp. on Unifying Theories of Programming (UTP). 2016. LNCS 10134

2015

• S. Foster and J. Woodcock: Mechanised Theory Engineering in Isabelle. NATO Advanced Study Institute on Dependable Software Systems Engineering. Eds: M. Irlbeck, D. Peled, and A. Pretschner. IOS Press, 2015
• S. Foster and G. Struth: On the Fine-Structure of Regular Algebra. Journal of Automated Reasoning 54:2. February 2015

2014

• J. Woodcock, A. Cavalcanti, J. Fitzgerald, S. Foster, P. G. Larsen: Contracts in CML. 6th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA). LNCS. October 2014
• S. Foster, F. Zeyda, and J. Woodcock: Isabelle/UTP: A Mechanised Theory Engineering Framework. 5th International Symposium on Unifying Theories of Programming. LNCS 8963. May 2014
• S. Foster, A. Miyazawa, J. Woodcock, A. Cavalcanti, J. Fitzgerald, P. G. Larsen: An approach for managing semantic heterogeneity in systems of systems engineering. IEEE 9th International Systems of Systems Engineering Conference. 2014
• S. Foster and G. Struth: Regular Algebras. Archive of Formal Proofs. 2014.
• L. D. Couto, S. Foster, and R. Payne: Towards Verification of Constituent Systems through Automated Proof. Workshop on Engineering Dependable Systems of Systems (EDSoS). April 2014

2013

• S. Foster and J. Woodcock: Unifying Theories of Programming in Isabelle. ICTAC School on Software Engineering. 2013. LNCS 8050

2012

• S. Foster and G. Struth: Automated Analysis of Regular Algebra. 6th International Joint Conference on Automated Reasoning (IJCAR). 2012. LNCS 7364
• S. Foster, O. Rypáček, and G. Struth: Correctness of Object Oriented Models by Extended Type Inference. 9th Intl. Colloquium on Theoretical Aspects of Computing (ICTAC). 2012. LNCS 7521
• A. Armstrong, S. Foster and G. Struth: Dependently Typed Programming Based on Automated Theorem Proving. 11th Intl. Conference on Mathematic of Program Construction (MPC). 2012. LNCS 7342
• S. Foster, G. Struth, and T. Weber: Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL. Proc. 12th Intl. Conf. on Relational and Algebraic Methods in Computer Science (RAMiCS). 2012. LNCS 6663.

2011 and before

• S. Foster, G. Struth: Integrating an Automated Theorem Prover into Agda. 3rd NASA Formal Methods Symposium (NFM). 2011. LNCS 6617
• S. Foster: A Compositional Semantic Theory for Service Composition. PhD Thesis, University of Sheffield. January 2010.
• B. Norton, S. Foster, Andrew Hughes: A Compositional Operational Semantics for OWL-S. Intl. Workshop on Web Services and Formal Methods (WS-FM). 2005. LNCS 3670