|
CS Home
Dept Info/Contacts
People
Research
Events
Courses
Undergrad Programs:
Computer Science
Informatics
Graduate Program
Prospective Students
Faculty Hiring
Employment
Resources
Help Lab Hours
Student Groups
Support the Department: Weeg Professorship
|
|
KeY: A Formal Method for Object-Oriented Software
Friday, March 13, 2009
4:00-5:00pm, 140 SH
Abstract
The success of embedded computer systems and of mobile devices leads to
an increasing demand for software programs that become more complex,
more safety or security critical, and that are expected to be produced
in shorter time and with less effort. Developing methods to satisfy this
demand is one of the main challenges in software engineering. One
paradigm to improve software quality is to analyse programs with the
help of deductive and formal methods.
KeY is an approach (and a system) for the deductive verification of
object-oriented software written in the Java. It aims for integrating
design, implementation, formal specification and formal verification as
seamlessly as possible. The intention is to provide a platform that
allows close collaboration of conventional and formal software
development methods. This talk gives an overview of the KeY approach and
highlights the main features of the KeY system, in particular the
different specification languages that are supported, the different user
interfaces that are offered for authoring proofs, and the first-order
dynamic logic underlying the approach.
|
