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