Assured Software Engineering and Proof
Apply logic to solve software engineering problems, and learn how to engineer computer systems that are correct and free of bugs.
This four-day course teaches participants state-of-the-art techniques in assured development. It will use model-based engineering and formal methods which are essential in the development of safety- and security-critical systems.
We will focus on the Isabelle system, which harnesses advanced techniques including functional programming, deductive proof, automated verification and code generation. By the end of the course, you will be able to apply techniques such as automated theorem proving and model checking in assured development.
Course information
- Dates of next course: Spring 2025 (dates to be confirmed in November 2024).
- Course fee: £2,500 (VAT exempt)
Who is this course for?
This course is suitable for:
- Practitioners across all domains including aerospace, military, railway, automotive, civil nuclear, civil maritime, medical devices and healthcare;
- Developers of equipment safety cases during design for software, hardware, procedures, systems and/or platforms;
- Developers of safety cases for operational safety and disposal;
- Reviewers of safety cases within an organisation or as an independent activity;
- Developers and reviewers of changes to existing safety-critical / safety-related equipment and operations;
- Project managers where development of a safety case is a significant element of projects they manage;
- Regulators of safety critical domains.
Prerequisites
Participants should hold a Bachelor's degree in Computer Science, or equivalent.
If you are unsure about your previous experience, please email the CPD Team at cs-cpd@york.ac.uk so that we can assess your suitability for this course.
Contact us
Short courses in systems safety engineering; MSc Safety Critical Systems Engineering
Toshiko Smith, Postgraduate Student Services Team
cs-safety-courses@york.ac.uk
01904 325536
Bespoke courses for industry; Short course: Assured Software Engineering and Proof
Tom Rawle, Business and Partnerships Team
cs-cpd@york.ac.uk
01904 323561
Short course: Generative AI in Engineering and Manufacturing
University of York CPD team
Learning outcomes
On this course you will:
- Understand how model-based engineering benefits from formal verification techniques;
- Apply interactive theorem proving using the Isabelle system;
- Write and verify functional programs using theorem proving in Higher Order Logic;
- Model, animate and verify systems using specifications with pre- and post-conditions in the Z notation;
- Apply techniques such as refinement and promotion to support stepwise development of models and programs.
Recommended reading
- Nikow, T. and Klein, G. Concrete Semantics with Isabelle/HOL. http://concrete-semantics.org/
- Woodcock J.C.P. and Davies J., Using Z: specification, refinement and proof, Prentice-Hall International, 1996
How is this course taught?
This short course is led by Dr Simon Foster and Dr Pedro Ribeiro, who are based in the Department of Computer Science at the University of York. Collectively, they have over 20 years of experience collaborating with industrial partners at the forefront of cutting-edge research.
The course will be taught over four days. Half of your time will be spent in lectures, where theory documents for the Isabelle system will serve as interactive lecture notes. You will spend the other half of your time in problem-based learning classes, where you will put into practice the theoretical knowledge you have learned.
Typically, the problem classes will be composed of Isabelle-based exercises, which will be tackled in teams, with answers presented to the whole group afterwards.
Dr Simon Foster
Dr Simon Foster is a lecturer in Computer Science at the University of York, and a member of the Software Engineering for Robotics group. He is an expert in interactive theorem proving using Isabelle/HOL, formal verification, and process algebra.
Simon has worked extensively on EU research projects with industrial collaboration, and has recently completed a three-year EPSRC-UKRI fellowship on assurance of cyber-physical systems (CyPhyAssure). He leads the development of Isabelle/UTP, a practical theorem prover for heterogeneous systems, which he has applied to verification of reactive and hybrid systems. He has also developed Isabelle/SACM, an assurance case tool with evidence coming from multiple formal verification tools in Isabelle.
Simon gained his PhD at the University of Sheffield in 2010, which developed a timed process algebra for Web service composition semantics.
Dr Pedro Ribeiro
Dr Pedro Ribeiro is a lecturer in Computer Science. Previously, he was a Research Fellow in the School of Physics, Engineering and Technology and before that a Research Associate, both at the University of York.
He has over a decade of experience working on formal methods with applications in modern software engineering approaches. He completed his PhD in 2015 on the foundations of angelic nondeterminism, and his research interests span the breadth of the engineering lifecycle, including design and development of domain-specific notations and their semantics, testing, and formal verification using automated mathematical proof techniques.
Pedro is a member of the Software Engineering for Robotics Research Group, which is the hub for RoboStar - a centre of excellence in Software Engineering for Robotics. Pedro is also a founding member of Formal Methods Europe's communications committee.
"A really good course, which helped my understanding of the methods and specific tools. I definitely gained more knowledge and a better understanding of the formal methods and application within the industry domain.
I would recommend this course to others if they want to gain a deeper understanding of the complexities of formal methods."
Software Assurance Engineer, Jacobs
Book your place
- Course fee: £2,500 (VAT exempt)
- To make a group booking please contact cs-cpd
@york.ac.uk.
The price includes all course materials. We will provide a booking form when the next course dates are confirmed.
Before you make your booking, please ensure that you have read our booking conditions, below. Please complete and return your booking form to cs-cpd
Note: you only need to complete the short booking form, above, and not the booking forms found on the online payment page.
Accommodation
Participants are responsible for booking their own accommodation and arranging payment directly with the hotel of their choice.
A list of some hotel options in the city will be circulated to all delegates. For further information about York, please visit the Visit York website.
Booking conditions
- Acceptance onto a short course is at the agreement of the course leader. They will want to assure themselves that you have the relevant level of background knowledge. You may therefore be asked to provide a CV detailing your knowledge / experience in particular areas.
- Course fees quoted include all relevant course materials, tuition, lunch and refreshments.
- For your place to be confirmed, a completed booking form with Purchase Order or payment is required before the course start date.
- Fees are payable to The University of York. Cheques should be drawn on a UK bank in pounds sterling and made payable to The University of York. Payment may also be made by Visa or Mastercard.
Cancellations
We regret that a fee must be charged when confirmed bookings are cancelled or transferred to future dates. In the event of a cancellation, you may nominate a substitute (acceptance of this substitution is subject to academic and availability conditions). If a suitable substitute cannot be found the following scale of charges will apply:
- 56 days or more before the course starts ‐ full refund
- 55 days or less ‐ 50% refund
- 28 days or less ‐ 25% refund
- 14 days or less ‐ no refund
We reserve the right to amend published information.
Contact us
Short courses in systems safety engineering; MSc Safety Critical Systems Engineering
Toshiko Smith, Postgraduate Student Services Team
cs-safety-courses@york.ac.uk
01904 325536
Bespoke courses for industry; Short course: Assured Software Engineering and Proof
Tom Rawle, Business and Partnerships Team
cs-cpd@york.ac.uk
01904 323561
Short course: Generative AI in Engineering and Manufacturing
University of York CPD team