Formal Verification of Object-oriented Software
Peter H. Schmitt (Universitaet Karlsruhe)
NICTA LC SEMINARDATE: 2009-02-05
TIME: 14:00:00 - 15:00:00
LOCATION: NICTA - 7 London Circuit
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
This talk will focus on verification methodologies using symbolic execution as opposed to other possible and successful verification techniques. The presentation will be centered around the KeY software verification tool jointly developed at Universitat Karlsruhe, Universitat Koblenz and Chalmers University of Technology. In a first part we will walk through a small verification example. This will give us the opportunity to explain the basic concepts and steps hands-on. This part will also include a live demo of the KeY system. In a second part we will have a look a some advanced issues and perspectives for future research and development.
