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