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., 8 Sept 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 › Conference contribution

  Open Access

  File
• 2022

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

• 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

• 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

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

  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

• Probabilistic Semantics for RoboChart A Weakest Completion Approach

  Woodcock, J. 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, J. 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, J. 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
• 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

• 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, J. 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
• 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
• 2014

  An approach for managing semantic heterogeneity in Systems of Systems Engineering

  Foster, S., Miyazawa, A., Woodcock, J. C. P., Cavalcanti, A. L. C., Fitzgerald, J. & Larsen, P. G., 2014, 9th International Conference on Systems of Systems Engineering (2014). Cook, S., Ireland, V., Gorod, A., Ferris, T. & Do, Q. (eds.). IEEE, p. 113-118 6 p. (IEEE Systems Journal).

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

• Contracts in CML

  Woodcock, J. C. P., Cavalcanti, A. L. C., Fitzgerald, J., Foster, S. & Larsen, P. G., 2014, 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Springer, p. 54-73 20 p. (Lecture Notes in Computer Science; vol. 8803).

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

  Open Access

  File

• Towards Verification of Constituent Systems through Automated Proof

  Foster, S. D., 7 May 2014, Workshop on Engineering Dependable Systems of Systems. ACM

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

  Open Access
• 2013

  Unifying Theories of Programming in Isabelle

  Foster, S. & Woodcock, J., 2013, Unifying Theories of Programming and Formal Engineering Methods - International Training School on Software Engineering, Held at ICTAC 2013, Shanghai, China, August 26-30, 2013, Advanced Lectures. Liu, Z., Woodcock, J. & Zhu, H. (eds.). Springer, Vol. 8050. p. 109-155 47 p. (Lecture Notes in Computer Science).

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

  File