Simon David Foster

Search results

• 2023

  Automated Compositional Verification for Robotic State Machines using Isabelle/HOL

  Yan, F., Foster, S. D. & Habli, I., 16 Mar 2023, (Accepted/In press) 27th International Conference on Engineering of Complex Computer Systems. IEEE

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL

  Foster, S. D. & Wolff, B., 16 Mar 2023, (Accepted/In press) The 27th Internation Conference on Engineering of Complex Computer Systems (ICECCS 2023). IEEE

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• UTP, Circus, and Isabelle

  Woodcock, J., Cavalcanti, A., Foster, S., Oliveira, M., Sampaio, A. & Zeyda, F., 2023, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Science and Business Media Deutschland GmbH, p. 19-51 33 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14080 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Chapter
• 2022

  Assurance Case Process of RoboChart Supported by Formal Verification

  Yan, F., Foster, S. D. & Habli, I., 2022, (Unpublished).

  Research output: Contribution to conference › Poster

  File

• Formally Verified Animation for RoboChart Using Interaction Trees

  Ye, K., Foster, S. & Woodcock, J., 10 Oct 2022, Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Proceedings. Riesco, A. & Zhang, M. (eds.). Springer, p. 404-420 17 p. (Lecture Notes in Computer Science ; vol. 13478).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Model-Based Generation of Hazard-Driven Arguments and Formal Verification Evidence for Assurance Cases

  Yan, F., Foster, S. D., Habli, I. & Wei, R., 6 Feb 2022, 10th International Conference on Model-Driven Engineering and Software Development. SciTePress, p. 252-263 12 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Verifying and Assuring Robotic Systems with Isabelle/UTP

  Foster, S. D., 11 Oct 2022.

  Research output: Contribution to conference › Poster

  Open Access

  File
• 2021

  Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving

  Ye, K., Foster, S. & Woodcock, J., 22 Oct 2021, Relational and Algebraic Methods in Computer Science - 19th International Conference, RAMiCS 2021, Proceedings. Fahrenberg, U., Gehrke, M., Santocanale, L. & Winter, M. (eds.). Springer, p. 465-482 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13027 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Automated verification of reactive and concurrent programs by calculation

  Foster, S., Ye, K., Cavalcanti, A. & Woodcock, J., 14 Apr 2021, In: Journal of Logical and Algebraic Methods in Programming. 121, 100681.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

• Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL

  Foster, S., Hur, C-K. & Woodcock, J., 13 Aug 2021, International Conference on Concurrency Theory (CONCUR 2021). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, (LIPIcs).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs

  Foster, S. D., Munive, J. H. Y., Struth, G. & Gleirscher, M., 10 Nov 2021, Formal methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings. Springer, p. 367-386 18 p. (Lecture Notes in Computer Science; vol. 13047).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM

  Foster, S. D., Nemouchi, Y., Gleirscher, M., Wei, R. & Kelly, T., Dec 2021, In: Formal Aspects of Computing. 33, 6, p. 855-884

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

• Probabilistic modelling and verification using RoboChart and PRISM

  Ye, K., Cavalcanti, A., Foster, S., Miyazawa, A. & Woodcock, J., 3 Oct 2021, In: Software and Systems Modeling.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

• Robostar technology: Modelling uncertainty in robochart using probability

  Woodcock, J., Foster, S., Mota, A. & Ye, K., 5 Jul 2021, Software Engineering for Robotics. Springer International Publishing AG, p. 413-465 53 p.

  Research output: Chapter in Book/Report/Conference proceeding › Chapter

• Safety Case Generation by Model-based Engineering: State of the Art and a Proposal

  Yan, F., Foster, S. & Habli, I., 18 Apr 2021, The Eleventh International Conference on Performance, Safety and Robustness in Complex Systems and Applications, proceedings. International Academy, Research, and Industry Association , p. 4-7 4 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File
• 2020

  Automated Algebraic Reasoning for Collections and Local Variables with Lenses

  Foster, S. D. & Baxter, J., 1 Apr 2020, 18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020). Springer, 16 p. (Lecture Notes in Computer Science).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Automated Verification of Reactive and Concurrent Programs by Calculation

  Foster, S., Ye, K., Cavalcanti, A. & Woodcock, J., 27 Jul 2020.

  Research output: Working paper › Preprint

  File

• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL

  Munive, J. H. Y., Struth, G. & Foster, S. D., 1 Apr 2020, 18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020). Springer, 16 p. (Lecture Notes in Computer Science).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study

  Foster, S. D., Nemouchi, Y., O'Halloran, C., Tudor, N. & Stephenson, K., 7 Oct 2020, FormaliSE '20: Proceedings of the 8th International Conference on Formal Methods in Software Engineering. ACM

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Towards Formal Verification of Control Algorithms for Autonomous Marine Vehicles

  Foster, S. D., Gleirscher, M. & Calinescu, R., 2 Aug 2020, (Accepted/In press) Proceeding of the 25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020). IEEE, 6 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP

  Foster, S. D., Baxter, J., Cavalcanti, A. L. C., Woodcock, J. & Zeyda, F., 26 Jun 2020, (E-pub ahead of print) In: Science of Computer Programming. 197, 40 p., 102510.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

• Unifying Theories of Reactive Design Contracts

  Foster, S. D., Cavalcanti, A. L. C., Canham, S. J., Woodcock, JAMES. C. P. & Zeyda, F., 8 Jan 2020, In: Theoretical Computer Science. 802, p. 105-140

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File
• 2019

  Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

  Ye, K., Foster, S. D. & Woodcock, JAMES. C. P., 30 May 2019, From Astrophysics to Unconventional Computation. Springer, p. 215-254 40 p.

  Research output: Chapter in Book/Report/Conference proceeding › Chapter

• Evolution of Formal Model-based Assurance Cases for Autonomous Robots

  Gleirscher, M., Foster, S. D. & Nemouchi, Y., 9 Sept 2019, Software Engineering and Formal Methods. Springer, p. 87-104 18 p. (Lecture Notes in Computer Science; vol. 11724).

  Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

  Open Access

  File

• Hybrid Relations in Isabelle/UTP

  Foster, S. D., 23 Sept 2019, 7th International Symposium on Unifying Theories of Programming (UTP). Springer, p. 130-153 24 p. (Lecture Notes in Computer Science; vol. 11885).

  Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

  Open Access

  File

• Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods

  Nemouchi, Y., Foster, S. D., Gleirscher, M. & Kelly, T. P., 22 Nov 2019, (E-pub ahead of print) Integrated Formal Methods: Proceedings of the 15th International Conference. Springer, Vol. 11918. p. 379-398 20 p. (LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming

  Foster, S. D., Zeyda, F., Nemouchi, Y., De Oliveira Salazar Ribeiro, P. F. & Wolff, B., 11 Jun 2019, In: Archive of Formal Proofs. 168 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

• New Opportunities for Integrated Formal Methods

  Gleirscher, M., Foster, S. & Woodcock, J., 23 Oct 2019, In: ACM Computing Surveys. 52, 16, 117.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

• Probabilistic Semantics for RoboChart A Weakest Completion Approach

  Woodcock, JAMES. C. P., Cavalcanti, A. L. C., Foster, S. D. & Mota, A., 4 Nov 2019, 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. Ribeiro, P. & Sampaio, A. (eds.). Springer, (Lecture Notes in Computer Science; vol. 11885).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  File
• 2018

  Automating Verification of State Machines with Reactive Designs and Isabelle/UTP

  Foster, S. D., Baxter, J. E., Cavalcanti, A. L. C., Miyazawa, A. H. & Woodcock, JAMES. C. P., 5 Oct 2018, 15th International Conference on Formal Aspects of Component Software. Ölveczky, P. C. & Bae, K. (eds.). Springer, p. 137-155 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11222 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra

  Foster, S. D., Ye, K., Cavalcanti, A. L. C. & Woodcock, JAMES. C. P., 1 Nov 2018, Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Proceedings. Guttmann, W., Desharnais, J. & Joosten, S. (eds.). Springer, Vol. 11194. p. 205-224 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11194 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Compositional Assume-Guarantee Reasoning of Control Law Diagrams using UTP

  Ye, K., Foster, S. D. & Woodcock, JAMES. C. P., Apr 2018, (Unpublished) 202 p.

  Research output: Working paper

  File

• Generalised Reactive Processes in Isabelle/UTP

  Foster, S. D. & Canham, S. J., 6 Apr 2018, (Unpublished) 56 p.

  Research output: Working paper

  File

• Isabelle/UTP: Mechanised Theory Engineering for the UTP

  Foster, S. D., Zeyda, F., Nemouchi, Y., De Oliveira Salazar Ribeiro, P. F. & Wolff, B., 4 Apr 2018, (Unpublished) 162 p.

  Research output: Working paper

  File

• Kleene Algebra in Unifying Theories of Programming

  Foster, S. D., 5 Apr 2018, (Unpublished) 6 p.

  Research output: Working paper

  File

• Reactive Designs in Isabelle/UTP

  Foster, S. D., Baxter, J. E., Cavalcanti, A. L. C., Woodcock, JAMES. C. P. & Canham, S. J., 6 Apr 2018, (Unpublished) 108 p.

  Research output: Working paper

  File

• Stateful-Failure Reactive Designs in Isabelle/UTP

  Foster, S. D., Baxter, J. E., Cavalcanti, A. L. C. & Woodcock, JAMES. C. P., 17 Apr 2018, (Unpublished).

  Research output: Working paper

  File

• Theory of Designs in Isabelle/UTP

  Foster, S. D., Nemouchi, Y. & Zeyda, F., 6 Apr 2018, (Unpublished) 47 p.

  Research output: Working paper

  File

• Unifying Theories of Time with Generalised Reactive Processes

  Foster, S. D., Cavalcanti, A. L. C., Woodcock, JAMES. C. P. & Zeyda, F., Jul 2018, In: Information Processing Letters. 135, p. 47-52 6 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File
• 2017

  Formalising Cosimulation Models

  Zeyda, F., Ouy, J., Foster, S. D. & Cavalcanti, A. L. C., Sept 2017, (E-pub ahead of print) 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems (CoSim-CPS 2017). 15 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Optics in Isabelle/HOL

  Foster, S. D. & Zeyda, F., 1 Jun 2017, In: Archive of Formal Proofs. p. 1-28 28 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

• Towards a UTP semantics for modelica

  Foster, S., Thiele, B., Cavalcanti, A. & Woodcock, J., 1 Jan 2017, Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers. Bowen, J. P. & Zhu, H. (eds.). Springer, p. 44-64 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10134 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL

  Foster, S. D. & Woodcock, JAMES. C. P., 9 Jan 2017, Concurrency, Security, and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. Springer, Vol. 10160. p. 39-64 26 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10160).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• UTP By Example: Designs

  Woodcock, JAMES. C. P. & Foster, S. D., 6 Apr 2017, Engineering Trustworthy Software Systems: Second International School, SETSS 2016 Chongqing. Jonathan P., B., Liu, Z. & Zhang, Z. (eds.). Springer, Vol. LNCS 10215. p. 16-50 35 p.

  Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

  Open Access

  File
• 2016

  An Axiomatic Value Model for Isabelle/UTP

  Zeyda, F., Foster, S. D. & Freitas, L., 2016, (Accepted/In press) 6th International Symposium on Unifying Theories of Programming. p. 1-20 20 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Heterogeneous semantics and unifying theories

  Woodcock, J., Foster, S. & Butterfield, A., 5 Oct 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Margaria, T. & Steffen, B. (eds.). Springer, p. 374-394 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9952 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Heterogeneous Semantics and Unifying Theories

  Woodcock, J., Foster, S. D. & Butterfield, A., 2016, (Accepted/In press) 7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation. p. 374-394 21 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Towards Semantically Integrated Models and Tools for Cyber-Physical Systems Design

  Larsen, P. G., Fitzgerald, J., Woodcock, J., Nilsson, R., Gamble, C. & Foster, S. D., Oct 2016, 7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation. p. 171-186 16 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Unifying heterogeneous state-spaces with lenses

  Foster, S., Zeyda, F. & Woodcock, J., 24 Oct 2016, Theoretical Aspects of Computing - ICTAC 2016, 13th International Colloquium, Proceedings. Wang, F. & Sampaio, A. (eds.). Springer, p. 295-314 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9965 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File
• 2015

  Isabelle/UTP: A Mechanised Theory Engineering Framework

  Foster, S., Zeyda, F. & Woodcock, J., 6 Jan 2015, Unifying Theories of Programming : 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers. Naumann, D. (ed.). Springer, Vol. 8963. p. 21-41 21 p. (Lecture Notes in Computer Science).

  Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

  Open Access

  File