Dilian Gurov: Modular Verification of Temporal Safety Properties of Procedural Programs
Dilian Gurov, Theory Group, KTH CSC
Time: Mon 2013-02-11 12.10 - 13.00
Location: Room 4523, Lindstedtsvägen 5, 5th floor, KTH CSC
Lunch is served at 12:00 noon (register at doodle.com/mbngq5qt8mw6puhe by Thu Feb 7 at 8 pm). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for roughly one more hour of a possibly slightly more technical presentation.
Abstract
Modularity as a software design principle aims at controlling the complexity of developing and maintaining large software. When applied to verification, modularity means that the individual modules are specified and verified independently of each other, while global, system-wide properties are verified relative to the specifications of the modules rather than to their implementatons. Such a relativization is the key to verifying sofware in the presence of variability, that is, of modules the implementation of which is expected to either evolve or be dynamically upgraded, or is not even available at verification time, or exists in multiple versions as resulting from a software product line.
In this tutorial I will present modular verification in the context of temporal safety properties and a program model of recursive programs that abstracts away from data. The proposed method is algorithmic and is based on the construction of maximal program models that replace the local specifications when verifying global properties.