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