Thursday, December 3, 2009
Sriram Rajamani, Researcher, Microsoft, IndiaVerification, Testing and Statistics
Abstract: We present work by the RSE group at MSR India. We start by describing Yogi, a property checker that combines static and ...
Friday, October 30, 2009
Francesco Logozzo, Researcher, Microsoft, USAPrecise and scalable static analysis of bytecode with Clousot & Code Contracts
Abstract: I will discuss the goals and the internals of Clousot, the static analyzer based on abstract interpretation that we have...
Tuesday, October 27, 2009
Roberto Bagnara, Researcher, University of Parma, ItalyRanking Functions for Automatic Termination Analysis
Abstract: Automated termination analysis of software programs has been a hot research topic for two decades. And still it is, as w...
Monday, October 26, 2009
Alan Mycroft, Invited researcher, University of Cambridge, United KingdomStrictness Meets Data Flow
Abstract: Properties of programs can be formulated using various techniques: dataflow analysis, abstract interpretation and type-l...
Tuesday, October 20, 2009
Murdoch Gabbay, Researcher, Heriot-Watt University, United KingdomPermissive Nominal Terms
Abstract: One area which has consistently thrown up challenges in computer science has been the treatment of names and binding. Na...
Wednesday, October 14, 2009
Uri Juhasz, Researcher, Tel Aviv University, IsraelModular Analysis of Shared Abstractions
Abstract: One of the main difficulties with modular analysis is the issue of aliasing. Several systems have been proposed that all...
Monday, October 5, 2009
Alvaro Arenas, Researcher, E-Science Centre, STFC Rutherford Appleton Laboratory, United KingdomUsage Control and Reputation in Grid Systems
Abstract: Collaborative systems such as Grids enable seamless resource sharing across multiple organisations, constituting the bas...
Wednesday, September 23, 2009
Martin Leucker, Researcher, Institut für Informatik, Technische Universität München, GermanyDon't Know for Multi-Valued Systems
Abstract: Abstraction is one of the key techniques for model checking. In this presentation, we briefly review two-valued as well ...
Tuesday, September 22, 2009
Diego Garbervetsky, Professor, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad De Buenos Aires, Argentina.Invariant-based analysis of dynamic memory requirements
Abstract: In this talk I will present a series of techniques to automatically compute parametric certificates of dynamic memory ut...
Friday, September 18, 2009
Rob Hierons, Professor of Computing, School of Information Systems, Computing and Mathematics, Brunel University, Uxbridge, Middlesex, UKSearch Based Testing from State Machines
Abstract: Software testing is widely recognised to be an expensive, error prone and time consuming process and this has led to muc...
Thursday, June 25, 2009
Luis Moniz Pereira, Research Professor, Centro de Inteligencia Artificial (CENTRIA), Universidade Nova de Lisboa, PortugalOn Preferring and Inspecting Abductive Models
Abstract: This work proposes the application of preferences over abductive logic programs as an appealing declarative formalism to...
Tuesday, May 5, 2009
Pierre Ganty, Post-doctoral Researcher, University of California at Los Angeles, USAWhat's decidable for Asynchronous Programs?
Abstract: An asynchronous or “event-driven” program is one that contains procedure calls which are not directly execut...
Tuesday, April 28, 2009
Julia Lawall, Lektor, DIKU University of Copenhagen, DenmarkA Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking
Abstract: Reasoning about program control-flow paths is an important functionality of a number of recent program matching language...
Monday, April 27, 2009
Amal Ahmed, Research Assistant Professor, Toyota Technical Institute, Chicago, USALogical Relations: A Step Towards More Secure and Reliable Software
Abstract: Logical relations are a promising proof technique for establishing many important properties of programs, programming la...
Thursday, April 23, 2009
Zaynah Dargaye, PhD Student, INRIA Rocquencourt, FranceMechanized Verification of Functional Language Compiler
Abstract: In the context of mechanized verification of a compiler for a functional language, we have experienced the influence of ...
Monday, March 30, 2009
Laurent Mauborgne, Associate Professor, École Normale Supérieure, Paris, FranceDisjunctions that Scale Up
Abstract: The main difficulty in abstract interpretation is to handle disjunctions: on one hand, keeping precise disjunctive infor...
Wednesday, March 25, 2009
Deepak Garg, PhD candidate, Computer Science Departament, Carnegie Mellon University, USAApplying logic to Secure Computer Systems
Abstract: Logic is emerging as an important tool in the design and implementation of secure systems. It can be used not only to re...
Monday, March 23, 2009
Aleks Nanevski, Post-doctoral Researcher, Microsoft Research, Cambridge, United KingdomProgramming with Hoare Type Theory
Abstract: Two main properties make type systems an effective and scalable formal method. First, important classes of programming e...
Tuesday, March 17, 2009
Ralf Lämmel, Professor (W3), University of Koblenz-Landau, GermanyThe Expression Lemma
Abstract: Algebraic data types and catamorphisms (folds) play a central role in functional programming as they allow programmers t...
Thursday, March 5, 2009
Alexey Gotsman, PhD candidate, University of Cambridge, United KingdomModular verification of concurrent programs with heap
Abstract: Reasoning about concurrent programs is made difficult by the number of possible interactions between threads. This is es...