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