Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:StaRVOOrS: Combined Static and Runtime Verification of Object-Oriented Software
Speaker:Wolfgang Ahrendt
coming from:Chalmers University
Speakers Bio:Wolfgang Ahrendt is associate professor at Chalmers University of

Technology in Gothenburg, Sweden. His major interests are software
verification, theorem proving, and runtime verification. He one of the
people behind the KeY approach and system, and has recently co-edited
the book 'Deductive Software Verification - The KeY Book' (LNCS 100001).

Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Thursday, 9 November 2017
Time:11:00
Duration:90 Minutes
Location:Saarbr├╝cken
Building:E1 5
Room:029
Abstract
Static verification techniques are used to analyse and prove properties about programs before they are deployed. In particular, deductive
verification techniques often work directly on the source code and are used to verify data-oriented properties of all possible executions. In
contrast, runtime verification techniques have been extensively used for control-oriented properties, and analyse concrete executions that
occur in the deployed program. I present an approach in which data-oriented and control-oriented properties may be stated in a single formalism
amenable to both static and dynamic verification techniques. The specification language enhances a control-oriented property language
with data-oriented pre/postconditions. We show how such specifications can be analysed using a combination of the deductive verification system
KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY performs fully automated proof attempts, the resulting
partial proofs are analysed, and used to optimize the specification for efficient runtime checking.
Contact
Name(s):Annika Meiser
Phone:0681 9303 9105
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created by:Annika Meiser/MPI-SWS, 10/25/2017 10:51 AMLast modified by:Uwe Brahm/MPII/DE, 11/09/2017 07:00 AM
  • Annika Meiser, 10/25/2017 10:59 AM
  • Annika Meiser, 10/25/2017 10:55 AM -- Created document.