Abstract: Cybercriminals use different types of geographically distributed servers to run their operations such as C&C servers...

Abstract: Observational refinement between software library implementations is key to modular reasoning: knowing that any program ...

Abstract: 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...

Abstract: Side-channels can often be easily eliminated, however rarely are, as the cost for this is considerable. In practice, use...

Abstract: The “verified security” methodology is an emerging approach to build high assurance proofs about security pr...

Abstract: Since the mid ’80s, compiler writers for functional languages (especially lazy ones) have been writing papers abou...

Abstract: It will be presented a general framework for a quantitative predicate abstraction for stability analysis of hybrid syste...

Abstract: Computer-aided verification provides effective means of analyzing the security of cryptographic primitives. However, it ...

Abstract: We present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementation...

Abstract: Abstraction (in its various forms) is a powerful established technique in model-checking; still, when unbounded data-str...

Abstract: Energy consumption analysis of embedded programs requires the analysis of low-level program representations. This is cha...

Abstract: Side-channel attacks recover secret inputs to programs from physical characteristics of computations, such as execution ...

Abstract: Gradual typing aims at combining static and dynamic type checking by introducing a dynamic type and cast expressions. Th...

Abstract: This talk will introduce a novel abstraction technique and a model checking algorithm for analysing stability of a parti...

Abstract: EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. It...

Abstract: Constraint and logic programming languages offer programmers powerful, declarative ways to go about solving complex comp...

Abstract: Continuations are programming abstractions that allow for manipulating the “future” of a computation. Amongs...

Abstract: When the representation of a data structure changes we would expect that the behaviour of clients using the data structu...

Abstract: By my understanding, IMDEA works a lot on verification and checking. Iwill sketchnominal techniques and recent activity ...

Abstract: Nanevski in his PhD thesis introduced and studied Contextual Modal Theory Theory. This is a lambda-calculus based via th...

Abstract: Strong update — the assignments overwrite the contents of the target property, is essential for precise static analysis ...

Abstract: Resource analysis aims to derive tight bounds on the usage of some numerical property. It is instrumental in a wide rang...

Abstract: Hybrid systems refer to systems exhibiting mixed discrete-continuous behaviors and arise as a natural byproduct of the i...

Abstract: Modern object oriented languages like C# and JAVA enable developers to build complex application in less time. These lan...

Abstract: In many software projects quality assurance relies largely on testing. Often, this activity is performed in a crafty way...

Abstract: In this informal two-part talk I will present recent studies on systematic construction of control-flow analyses for hig...

Abstract: In 1978, Cousot and Halbwachs showed how to determine at compile-time linear relations among program variables. Various ...

Abstract: Regular Expressions (RE) are an algebraic formalism for expressing regular languages, widely used in string search and a...

Abstract: We study the verification of safety properties over symmetric parametrized systems. These systems consist on an arbitrar...

Abstract: Modern geo-replicated databases underlying large-scale Internet services guarantee immediate availability and tolerate n...