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