Iniciativa IMDEA
Resumen: Cybercriminals use different types of geographically distributed servers to run their operations such as C&C servers...
Resumen: Observational refinement between software library implementations is key to modular reasoning: knowing that any program ...
Resumen: We address the problem in which a client stores a large amount of data with an untrusted server in such a way that, at a...
Resumen: Side-channels can often be easily eliminated, however rarely are, as the cost for this is considerable. In practice, use...
Resumen: The “verified security” methodology is an emerging approach to build high assurance proofs about security pr...
Resumen: Since the mid ’80s, compiler writers for functional languages (especially lazy ones) have been writing papers abou...
Resumen: It will be presented a general framework for a quantitative predicate abstraction for stability analysis of hybrid syste...
Resumen: Computer-aided verification provides effective means of analyzing the security of cryptographic primitives. However, it ...
Resumen: We present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementation...
Resumen: Abstraction (in its various forms) is a powerful established technique in model-checking; still, when unbounded data-str...
Resumen: Energy consumption analysis of embedded programs requires the analysis of low-level program representations. This is cha...
Resumen: Side-channel attacks recover secret inputs to programs from physical characteristics of computations, such as execution ...
Resumen: Gradual typing aims at combining static and dynamic type checking by introducing a dynamic type and cast expressions. Th...
Resumen: This talk will introduce a novel abstraction technique and a model checking algorithm for analysing stability of a parti...
Resumen: EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. It...
Resumen: Constraint and logic programming languages offer programmers powerful, declarative ways to go about solving complex comp...
Resumen: Continuations are programming abstractions that allow for manipulating the “future” of a computation. Amongs...
Resumen: When the representation of a data structure changes we would expect that the behaviour of clients using the data structu...
Resumen: By my understanding, IMDEA works a lot on verification and checking. Iwill sketchnominal techniques and recent activity ...
Resumen: Nanevski in his PhD thesis introduced and studied Contextual Modal Theory Theory. This is a lambda-calculus based via th...
Resumen: Strong update — the assignments overwrite the contents of the target property, is essential for precise static analysis ...
Resumen: Resource analysis aims to derive tight bounds on the usage of some numerical property. It is instrumental in a wide rang...
Resumen: Hybrid systems refer to systems exhibiting mixed discrete-continuous behaviors and arise as a natural byproduct of the i...
Resumen: Modern object oriented languages like C# and JAVA enable developers to build complex application in less time. These lan...
Resumen: In many software projects quality assurance relies largely on testing. Often, this activity is performed in a crafty way...
Resumen: In this informal two-part talk I will present recent studies on systematic construction of control-flow analyses for hig...
Resumen: In 1978, Cousot and Halbwachs showed how to determine at compile-time linear relations among program variables. Various ...
Resumen: Regular Expressions (RE) are an algebraic formalism for expressing regular languages, widely used in string search and a...
Resumen: We study the verification of safety properties over symmetric parametrized systems. These systems consist on an arbitrar...
Resumen: Modern geo-replicated databases underlying large-scale Internet services guarantee immediate availability and tolerate n...
