IMDEA initiative
Abstract: In this talk, we present an efficient static analysis based on Abstract Interpretation that aims at proving the absence ...
Abstract: Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic so...
Abstract: Computer systems are often difficult to debug and understand. A common way of gaining insight into system behavior is to...
Abstract: Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and fo...
Abstract: It is notoriously difficult to make distributed systems reliable. This becomes even harder in the case of the widely-dep...
Abstract: The ASCENS project (http://www.ascens-ist.eu/) researches foundations of and software-engineering methods for ensembles ...
Abstract: Despite the benefits of cloud computing, its potential customers are concerned with data mismanagement risks that stem f...
Abstract: The automated generation of test cases for heap allocated, complex, structures is particularly difficult. Various state ...
Abstract:
Abstract: In the talk I will present a series of abstractions that can be used to obtain approximated verification algorithms for ...
Abstract: Model checking based on Craig’s interpolants ultimately relies on efficient engines, such as SMT-Solvers, to log p...
Abstract: Cyber Physical Systems (CPS) is a term broadly used to define systems in which the cyber world consisting of computation...
Abstract: Invariants play a key role in verifying properties of imperative programs. Inductive reasoning is essential to verifying...
Abstract: We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints...
Abstract: One of the key challenges in automated software verification is obtaining a conservative, yet sufficiently precise under...
Abstract: A path-sensitive static analysis considers each possible execution path through a program separately, potentially yieldi...
Abstract: Constraint solvers such as Boolean SAT or modular arithmetic solvers are increasingly playing a key role in the construc...
Abstract: Software is constantly modified during its life cycle, posing serious risks because changes might not behave as expected...
Abstract: We show how to extract sensitive cryptographic keys from a variety of commercially available tamper resistant cryptograp...
Abstract: Formal verification is described as the branch of computer science that formally establishes the correctness of systems....
Abstract: Managed languages such as Java and C# are being considered for use in hard real-time systems. A hurdle to their widespre...
Abstract: In security and compliance, it is often necessary to ensure that agents and systems comply to complex policies. An examp...
