A reliable internet connection − that is what users are looking for. Bahareh Badban, PhD student at CWI, studied methods to improve TCP, one of the most important protocols for Internet applications. She will defend her thesis 'Verification Techniques for Extensions of Equality' on 7 September 2006 at the Vrije Universiteit Amsterdam.
Bahareh Badban improved the TCP internet protocol by using theorem provers. These are computer programs that are able to prove mathematical rules (theorems) by automatic reasoning. This is an important subfield in formal methods. Bahareh Badban extended existing theorem provers in order to be able to verify large distributed systems. To establish the reliability of TCPs, Badban used the interactive theorem prover PVS, which requires a human user to give hints to the system.
