Proceedings
On Temporal and Separation Logics
There exist many success stories about the introduction of logics designed for the formal verification verification systems. Obviously, the introduction of temporal logics to computer science has been a major step in the development of model-checking techniques. More recently, separation logics extend Hoare logic for reasoning about programs with dynamic data structures, leading to many contributions on theory, tools and applications.
In this talk, we illustrate how several features of separation logics, for instance the key concept of separation, are related to similar notions in temporal logics. We provide formal correspondences (when possible) and present an overview of related works from the literature.
This is also the opportunity to present bridges between well-known temporal logics and more recent separation logics.
Database Technology for Processing Temporal Data
Despite the ubiquity of temporal data and considerable research on processing such data, database systems largely remain designed for processing the current state of some modeled reality. More recently, we have seen an increasing interest in the processing of historical or temporal data that capture the dynamics of the modeled reality. The SQL:2011 standard introduced some temporal features, and commercial
DBMSs have started to offer temporal functionalities in a step-by-step manner. The speaker argues that in order to fully leverage existing database technologies for temporal data, a more fundamental and comprehensive solution is needed. The talk will provide an overview about the support for temporal data in the SQL standard and in commercial database management systems. Then, a recently proposed framework is presented that offers comprehensive support for sequenced temporal queries and allows a tight integration into relational database systems, thereby taking advantage of existing query optimization and evaluation technologies. New challenges for processing temporal data arise with multiple dimensions of time andthe increasing amounts of data, including time series data that represent a special kind of temporal data.
Model Checking Strategic Ability: Why, What, and Especially: How?
Automated verification of discrete-state systems has been a hot topic in computer science for over 35 years. Model checking of temporal and strategic properties is one of the most prominent and most successful approaches here. I will present a brief introduction to the topic, and mention some relevant properties that one might like to verify this way.
Then, I will talk about some recent results on approximate model checking and model reductions, which can be applied to facilitate verification of notoriously hard cases.
