Decorative Blue BlockHOMEDecorative Gray Block
PROSPECTIVE STUDENTS

This section contains all the information regarding admission requirements, degrees offered and various taught modules.
Find out more

RESEARCH

Interested in a specific subfield within Computer Science? Explore our various research groups and their active staff members here.
Find out more

INDUSTRY & COMMUNITY

The department has a variety of industry partners and associated projects. It is also involved in community outreach projects throughout the year.
Find out more

CURRENT STUDENTS

Access all the information you need as a current student, including module work, timetables and regulations.
Find out more

 

SEMINAR on CSP-PROVER: 11 July, 11:30 h

In this talk, we discuss the generic architecture of the tool CSP-Prover, and some of its applications: Software Correctness is highly relevant in many safety- and mission- critical domains, such as banking, e-commerce, etc.

CSP-Prover was first introduced at TACAS'05. It provides a generic interactive theorem proving environment for the process algebra CSP. The tool is based on the theorem prover "Isabelle". Our Web-Page http://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html provides some sample case studies of theoretical and of industrial nature.

With the help of CSP-Prover we developed and verified the first complete axiomatic semantics for the CSP stable failures model (see CONCUR'06). The proof involves sequentialisation and normalisation of processes, also a new normal form needs to be introduced. Read more 

 
Markus Roggenbach

Markus Roggenbach

ADDITIONAL NEWS
No additional news.

Search the News Archive

QUICK LINKS
Honours Modules
Tutor Application
Mamelodi Students
Manage My Details

Comments or queries?
Send us your feedback.

Decorative Red Block