Peter O'Hearn

Thursday, December 2, 2010

Peter O'Hearn, Professor, Queen Mary, London University

On Separation, Session Types and Algebra

Abstract: This talk explores the relation between two formalisms and one algebraic framework for concurrency. Session Types and Co...


Peter O'Hearn

Tuesday, November 30, 2010

Peter O'Hearn, Professor, Queen Mary, London University

Abductive, Deductive and Inductive Reasoning about Resources

Abstract: I describe an automated reasoning method which approaches programs in a way inspired by the way that a scientist approac...


Francesco Zappa

Friday, November 5, 2010

Francesco Zappa, Researcher, INRIA Rocquencourt, France

Shared memory, an elusive abstraction

Abstract: Multiprocessors provide an abstraction of shared memory, accessible by concurrently executing threads, which supports a ...


Ben Livshits

Friday, October 29, 2010

Ben Livshits, Research Scientist, Microsoft Research

Finding Malware on a Web Scale

Abstract: In recent years, attacks that exploit vulnerabilities in browsers and their associated plugins have increased significan...


Kerstin Eder

Thursday, October 21, 2010

Kerstin Eder, Researcher, University of Bristol, United Kingdom

Research in Design Automation and Verification at CS in Bristol

Abstract: This presentation gives a broad overview of recent and ongoing work in the area of Design Automation and Verification at...


Jean-François Raskin

Tuesday, October 5, 2010

Jean-François Raskin, Professor, Université Libre de Bruxelles, Belgium

Antichain Algorithms for Finite Automata

Abstract: We present a general theory that exploits simulation relations on transition systems to obtain antichain algorithms for ...


Julien Bertrane

Monday, May 10, 2010

Julien Bertrane, Researcher, Computer Science Departament, Carnegie Mellon University, USA

Developing temporal abstract domains that prove the temporal specifications of reactive systems

Abstract: We consider the complex behaviors of embedded systems with several communicating imperfectly-clocked synchronous systems...


Ruy Ley-Wild

Monday, May 3, 2010

Ruy Ley-Wild, Researcher, Computer Science Departament, Carnegie Mellon University, USA

Programmable Self-Adjusting Computation

Abstract: In the self-adjusting computation model, programs can respond automatically and efficiently to input changes by tracking...


Xavier Rival

Tuesday, April 13, 2010

Xavier Rival, Researcher, École Normale Supérieure, Paris, France

Shape analysis using separating shape graphs

Abstract: The purpose of shape analysis is to infer properties about unbounded data structures, such as trees or lists. We will pr...


Emerson Murphy-Hill

Tuesday, April 6, 2010

Emerson Murphy-Hill, Researcher, University of British Columbia

Programmer-Friendly Software Restructuring Tools

Abstract: Tools that perform semi-automated software restructuring (refactoring) are currently under-utilized by programmers. If m...


Laurent Mauborgne

Wednesday, March 24, 2010

Laurent Mauborgne, Researcher, École Normale Supérieure, Paris, France

Segmented Relations

Abstract: The core mechanism of abstract interpretation based program analysis consists in approximating a process of collecting m...


Juan Caballero

Tuesday, March 23, 2010

Juan Caballero, Researcher, Carnegie Mellon University, USA

Binary Program Analysis and Model Extraction for Security Applications

Abstract: In this talk I present a platform to extract models of security-relevant functionality from program binaries, enabling m...


Saurabh Srivastava

Monday, March 22, 2010

Saurabh Srivastava, PhD candidate, University of Maryland, USA

Satisfiability-based Program Reasoning and Synthesis

Abstract: Today, software is ubiquitous—it is deployed on virtually all electronic devices, small and large, including those...


Zvonimir Rakamaric

Monday, March 15, 2010

Zvonimir Rakamaric, Researcher, University of British Columbia

Modular Verification of Shared-Memory Concurrent System Software

Abstract: Software is large, complex, and error-prone. The trend in hardware design of switching to multi-core architectures makes...


Viktor Vafeiadis

Friday, March 12, 2010

Viktor Vafeiadis, Researcher, University of Cambridge, United Kingdom

Towards full verification of concurrent libraries

Abstract: Modern programming platforms, such as Microsoft’s .NET, provide libraries of efficient concurrent data structures,...


Alexander Malkis

Monday, March 8, 2010

Alexander Malkis, Researcher, University of Freiburg, Germany

Abstract Threads

Abstract: Verification of large multithreaded programs is challenging. Automatic approaches cannot overcome the state explosion in...


Mark Marron

Tuesday, March 2, 2010

Mark Marron, Post-doctoral Researcher, IMDEA Software Institute

High-Level Heap Abstractions for Debugging Programs

Abstract: The identification, isolation, and correction of program defects require the understanding of both the algorithmic struc...


Boris Köpf

Monday, March 1, 2010

Boris Köpf, Researcher, Max Planck Institute for Software Systems, Saarbruecken, Germany

Quantitative Information-Flow Analysis - Automation and Applications

Abstract: Information-flow analysis is a powerful technique for reasoning about the sensitive information that is exposed by a pro...


Joshua Dunfield

Wednesday, February 24, 2010

Joshua Dunfield, Researcher, McGill University, Montreal

Verifying Functional Programs with Type Refinements

Abstract: Types express properties of programs; typechecking is specification checking. But the specifications expressed by conven...


Derek Dreyer

Tuesday, January 26, 2010

Derek Dreyer, Researcher, Max Planck Institute for Software Systems, Germany

A Modal Logic for Equational Reasoning in ML-Like Languages

Abstract: The method of logical relations is a classic technique for proving the equivalence of higher-order programs that impleme...


Sumit Gulwani

Tuesday, January 26, 2010

Sumit Gulwani, Researcher, Microsoft, USA

The Reachability-bound Problem

Abstract: The “reachability-bound problem” is the problem of finding a symbolic worst-case bound on the number of time...


Ruzica Piskac

Monday, January 25, 2010

Ruzica Piskac, PhD Student, EPFL, Switzerland

Combining Theories with Shared Set Operations

Abstract: We explore automated reasoning techniques for the non-disjoint combination of theories that share set variables and oper...


Sumit Gulwani

Monday, January 25, 2010

Sumit Gulwani, Researcher, Microsoft, USA

Dimensions in Program Synthesis

Abstract: In this talk, I will briefly describe some recent program synthesis projects that are motivated by various reasons: enab...


Thomas Wies

Monday, January 25, 2010

Thomas Wies, Post-doctoral Researcher, Institute of Science and Technology (IST)

Forward Analysis of Depth-Bounded Processes

Abstract: We study the verification of message passing systems that admit unbounded creation of threads and name mobility. Depth-b...


Stan Rosenberg

Monday, January 25, 2010

Stan Rosenberg, PhD candidate, Stevens Institute of Technology, Hoboken, USA

Local reasoning for Java programs and its automation

Abstract: Shared mutable objects are a cornerstone of the object-oriented paradigm. Modular reasoning remains a challenge. For exa...