IMDEA initiative
Abstract: We examine the problem of inferring invariants for parametrized systems. Parametrized systems are concurrent systems con...
Abstract: Malware is a serious problem on mobile devices. Our vision is a verified app store in which each application has been fo...
Abstract: In this talk we present the framework Failure Tabled Constraint Logic Programming by Interpolation, FTCLP (Gange et al. ...
Abstract: In this talk we present a constraint logic framework that combines backward and forward chaining. Concretely in this fra...
Abstract: In Service-Oriented Architecture (SOA), service compositions provide the key tool for building complex, flexible, distri...
Abstract: Most logics for stateful reasoning in a concurrent setting are designed around a parallel composition operator ||. Given...
Abstract: The talk will introduce the C11 weak memory model that defines the semantics of concurrent C/C++ programs, and will answ...
Abstract: I will present in this talk some insights about the formalization of mathematics, using the case study of a formal devel...
Abstract: I will present a mapping from OCL (Object Constraint Language) to first-order logic. This mapping allows us to reason on...
Abstract: Hybrid systems refer to dynamical systems exhibiting a mixed discrete and continuous behaviours. Such behaviors appear n...
Abstract: Bounded model checking (BMC) is an effective algorithmic method for the verification of finite state systems against tem...
Abstract: Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactical...
Abstract: How would one specify a correct behaviour of an optimistic fine-grained concurrent data structure? For more than twenty ...
Abstract: As asynchronous programming becomes more mainstream, program analyses capable of automatically uncovering programming er...
Abstract: The most common approach for solving the problem of optimal task scheduling is to use expected values of the variables t...
Abstract: Many concurrent libraries are parameterised, meaning that they implement generic algorithms that take another library as...
Abstract: Modern web applications are backed by geo-replicated data stores that offer highly available and low latency data access...
