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...