Iniciativa IMDEA
Resumen: This talk explores the relation between two formalisms and one algebraic framework for concurrency. Session Types and Co...
Resumen: I describe an automated reasoning method which approaches programs in a way inspired by the way that a scientist approac...
Resumen: Multiprocessors provide an abstraction of shared memory, accessible by concurrently executing threads, which supports a ...
Resumen: In recent years, attacks that exploit vulnerabilities in browsers and their associated plugins have increased significan...
Resumen: This presentation gives a broad overview of recent and ongoing work in the area of Design Automation and Verification at...
Resumen: We present a general theory that exploits simulation relations on transition systems to obtain antichain algorithms for ...
Resumen: We consider the complex behaviors of embedded systems with several communicating imperfectly-clocked synchronous systems...
Resumen: In the self-adjusting computation model, programs can respond automatically and efficiently to input changes by tracking...
Resumen: The purpose of shape analysis is to infer properties about unbounded data structures, such as trees or lists. We will pr...
Resumen: Tools that perform semi-automated software restructuring (refactoring) are currently under-utilized by programmers. If m...
Resumen: The core mechanism of abstract interpretation based program analysis consists in approximating a process of collecting m...
Resumen: In this talk I present a platform to extract models of security-relevant functionality from program binaries, enabling m...
Resumen: Today, software is ubiquitous—it is deployed on virtually all electronic devices, small and large, including those...
Resumen: Software is large, complex, and error-prone. The trend in hardware design of switching to multi-core architectures makes...
Resumen: Modern programming platforms, such as Microsoft’s .NET, provide libraries of efficient concurrent data structures,...
Resumen: Verification of large multithreaded programs is challenging. Automatic approaches cannot overcome the state explosion in...
Resumen: The identification, isolation, and correction of program defects require the understanding of both the algorithmic struc...
Resumen: Information-flow analysis is a powerful technique for reasoning about the sensitive information that is exposed by a pro...
Resumen: Types express properties of programs; typechecking is specification checking. But the specifications expressed by conven...
Resumen: The method of logical relations is a classic technique for proving the equivalence of higher-order programs that impleme...
Resumen: The “reachability-bound problem” is the problem of finding a symbolic worst-case bound on the number of time...
Resumen: We explore automated reasoning techniques for the non-disjoint combination of theories that share set variables and oper...
Resumen: In this talk, I will briefly describe some recent program synthesis projects that are motivated by various reasons: enab...
Resumen: We study the verification of message passing systems that admit unbounded creation of threads and name mobility. Depth-b...
Resumen: Shared mutable objects are a cornerstone of the object-oriented paradigm. Modular reasoning remains a challenge. For exa...
