Department of Computer Science
University of Oxford

Scalable Systems

It is desirable that any computer system meet its specifications, and for some applications critical. However, verifying systems of realistic size and complexity in itself requires the help of computers. Techniques are being developed which extend the classes of system which may be reasoned about using the CSP model checker FDR. Specifically, to include those whose parameterisations might lead to unboundedly large state spaces. Thus enabling the benefits of using a theorem prover to be gained in a model checking environment for certain types of scalable system.

Related projects

CSP Model Checking

Efficient verification of software with replicated components
Random Image
Random Image
Random Image