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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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