IMDEA initiative
Abstract: We present work by the RSE group at MSR India. We start by describing Yogi, a property checker that combines static and ...
Abstract: I will discuss the goals and the internals of Clousot, the static analyzer based on abstract interpretation that we have...
Abstract: Automated termination analysis of software programs has been a hot research topic for two decades. And still it is, as w...
Abstract: Properties of programs can be formulated using various techniques: dataflow analysis, abstract interpretation and type-l...
Abstract: One area which has consistently thrown up challenges in computer science has been the treatment of names and binding. Na...
Abstract: One of the main difficulties with modular analysis is the issue of aliasing. Several systems have been proposed that all...
Abstract: Collaborative systems such as Grids enable seamless resource sharing across multiple organisations, constituting the bas...
Abstract: Abstraction is one of the key techniques for model checking. In this presentation, we briefly review two-valued as well ...
Abstract: In this talk I will present a series of techniques to automatically compute parametric certificates of dynamic memory ut...
Abstract: Software testing is widely recognised to be an expensive, error prone and time consuming process and this has led to muc...
Abstract: This work proposes the application of preferences over abductive logic programs as an appealing declarative formalism to...
Abstract: An asynchronous or “event-driven” program is one that contains procedure calls which are not directly execut...
Abstract: Reasoning about program control-flow paths is an important functionality of a number of recent program matching language...
Abstract: Logical relations are a promising proof technique for establishing many important properties of programs, programming la...
Abstract: In the context of mechanized verification of a compiler for a functional language, we have experienced the influence of ...
Abstract: The main difficulty in abstract interpretation is to handle disjunctions: on one hand, keeping precise disjunctive infor...
Abstract: Logic is emerging as an important tool in the design and implementation of secure systems. It can be used not only to re...
Abstract: Two main properties make type systems an effective and scalable formal method. First, important classes of programming e...
Abstract: Algebraic data types and catamorphisms (folds) play a central role in functional programming as they allow programmers t...
Abstract: Reasoning about concurrent programs is made difficult by the number of possible interactions between threads. This is es...
