University of Oxford Logo University of OxfordSoftware Engineering - Home
On Facebook
Follow us on twitter
Linked in
Linked in
Google plus
Google plus
Stumble Upon
Stumble Upon
Machine-Assisted Software Engineering

Automation in the process of software development can result in significant gains in productivity. This course teaches a method - and associated toolkit - that supports such automation. The B-Method and B-Toolkit support formal specification, design, and code generation, as well as validation and verification. See also

Course dates

No future courses planned.


At the End of the course, students will be able to construct large software designs using a layered approach, and carry out a complete development from abstract specifications to running C code. They will also be able to animate and validate specifications, generate software modules, and create design documentation.


Basic specification concepts:
abstract machine notation; software modules; states and operations; proof obligations; substitutions; abstract machine initialisation; abstract machine parameterisation.
Specification construction:
Parallel substitutions as specification of operations; incremental specification construction techniques.
Program concepts:
algorithm development; sequencing; loops.
Program development:
data refinement; design techniques; layers of software; implementation; libraries.
Program generation:
entity relationship descriptions; rapid prototyping; test-bench generation.
Software engineering concepts:
separation of concerns; abstraction; information hiding; modularisation; stepwise refinement.
predicate notation; machine-assisted proving; set notation; relations; functions; sequences.


A working knowledge of discrete mathematics is assumed: Software Engineering Mathematics would be a suitable preparation.