Date | Teacher | Place | Topic | Lecture notes / comments |
05.08.2011 | Axel Simon | room 8459 PMA meeting room | Semantics-Based Design of Modular Type Inferences that Deliver Best Types: Hindley-Milner and Beyond | Abstract:The steady increase in expressiveness of type systems tends to clutter code with an excessive amount of type information which calls for the use of type inference. Several people have argued that a type inference should infer the best types possible within the given type discipline. We systematically construct such an inference for the Hindley-Milner type system by recasting type inference as a program analysis problem: We apply abstract interpretation theory to a denotational semantics and obtain typing rules that are correct by construction and abstract-complete in that they infer the best types. The resulting rules are a variant of Henglein's semi-unification--based inference rules. The notion of ``abstract complete'' is weaker than ``principal typings'' but we argue that the former delivers the same advantages and that the latter is not type system-agnostic.We then observe that the Hindley-Milner type system is modular and reduce this fact to three properties developed in the abstract interpretation literature, namely, complete transfer functions, a complete projection operation and a condensing domain. Given the state-of-the-art, only two abstract domains feature these properties while remaining tractable, namely Herbrand abstractions and Boolean functions. We conclude that any modular type inference that infers principal typings must be based on these two domains. |
26.08.2011 | Cristian Prisacariu | room 8459 PMA meeting room | Introduction | This is mandatory for registered students.We might have an invited talk from the FCT 2011 conference that is organized at IFI from 22 to 25 August. |
02.09.2011 | no seminar | room 8459 PMA meeting room | HATS project meetings | There are HATS project meetings where most PMA group is participating. There will be no seminar this Friday.k |
09.09.2011 | no seminar | room 8459 PMA meeting room | FACS 2011 symposium | This week there is the FACS symposium hosted at IFI. Much of PMA will attend that. Therefore there will be no seminar. |
16.09.2011 | Cristian Prisacariu | room 8459 PMA meeting room | TBA | |
23.09.2011 | TBA | room 8459 PMA meeting room | TBA | |
30.09.2011 | TBA | room 8459 PMA meeting room | TBA | |
07.10.2011 | Kyungmin Bae | room 8459 PMA meeting room | State/Event-based LTL Model Checking under Parametric Generalized Fairness | Abstract:In modeling a concurrent system, fairness constraints are usually considered at a specific granularity level of the system, leading to many different variants of fairness: transition fairness, object/process fairness, actor fairness, etc. These different notions of fairness can be unified by making explicit their parametrization over the relevant entities in the system as universal quantification. We propose a state/event-based framework as well as an on-the-fly model checking algorithm to verify LTL properties under universally quantified parametric fairness assumptions, specified by generalized strong/weak fairness formulas. It enables verification of temporal properties under fairness conditions associated to dynamic entities such as new process creations. We have implemented our algorithm within the Maude system. |
14.10.2011 | Martin Steffen | room 8459 PMA meeting room | Estimating Resource Bounds for Software Transactions | Extended abstractis is available at the link belowpaper |
21.10.2011 | Hallstein Hansen | room 8459 PMA meeting room | "A reachability checker for planar, polygonal hybrid systems using incomplete acceleration" | |
28.10.2011 | no presentation | room 8459 PMA meeting room | NWPT workshop in Sweeden | Many PMA members attend the NWPT workshop in Sweden. |
04.11.2011 | Lizeth Tapia | room 8459 PMA meeting room | Dynamic Object Reclassification | Abstract:Reclassification changes the class membership of an object at run-time while retaining its identity. This presentation introduces a language with features for object reclassification. The approach is presented through the language FickleII which extends an imperative, typed, class-based, object-oriented language, where objects may be reclassified across classes with different members, so there will never be an attempt to access nonexisting members.Paper |
11.11.2011 | Cristian Prisacariu | room 8459 PMA meeting room | Quotienting and Compositional Model Checking | |
18.11.2011 | Eric Bodden (Germany) | room 8459 PMA meeting room | "Modular Reasoning in Aspect-Oriented Programs through Join Point Interfaces" | Abstract:Important security concerns, such as access control and runtime monitoring can be conveniently implemented using aspect-oriented programming languages. While aspect-oriented programming supports the modular definition of such crosscutting concerns, most approaches to aspect-oriented programming fail, however, to improve, or even preserve, modular reasoning. The main problem is that aspects usually carry, through their pointcuts, explicit references to the base code. These dependencies make programs fragile and hard to reason about. In this talk, we discuss how to separate base code and aspects using Join Point Interfaces, which are contracts between aspects and base code. Base code can define pointcuts that expose selected join points through a Join Point Interface. Conversely, an aspect can offer to advise join points that provide a given Join Point Interface. Crucially, however, aspect themselves cannot contain pointcuts, and hence cannot refer to base code elements. In addition, we will discuss Closure Joinpoints, a mechanism that allows base code to explicitly announce events to aspects. We will discuss why many previous attempts to defining such a language construct fail, and how Closure Joinpoints integrate with Join Point Interfaces to yield a language construct with a clear semantics, avoiding unwanted surprises. |
25.11.2011 | Saif Shams | room 8459 PMA meeting room | "Modeling and Performance Analysis of BitTorrent-Like Peer-to-Peer Networks" | Abstract:"In this paper, we develop simple models to study the performance of BitTorrent, a second generation peer-to-peer (P2P) application. We first present a simple fluid model and study the scalability, performance and efficiency of such a file-sharing mechanism. We then consider the built-in incentive mechanism of BitTorrent and study its effect on net-work performance. We also provide numerical results based on both simulations and real traces obtained from the Internet." paper from SIGCOM 2004 by Dongyu Qiu and R. Srikant |
02.12.2011 | Volker Stolz | room 8459 PMA meeting room | Practical Semantics Engineering with Ott | Abstract:In a short demo (based on our work-in-progress) I will illustrate how the Ott-tool [1] could make your life easier by
|
09.12.2011 | TBA | room 8459 PMA meeting room | TBA | Abstract: |
Teaching plan
Publisert 23. juni 2011 17:16
- Sist endret 29. nov. 2011 09:32