IMDEA initiative
Abstract: Different evaluation orders for the untyped(1) lambda-calculus exists (call-by-value, call-by-name, normal order, applic...
Abstract: Types provide a convenient and accesible mechanism for specifying program invariants. Dependent types extends simple typ...
Abstract: There is a growing interest in the use of UML for the modeling of embedded and hybrid systems. A key factor for the adop...
Abstract: We present a framework that unifies unit testing and run-time verification (as well as static verification and static de...
Abstract: The definition of type equivalence plays a crucial role in any statically typed language. In dependent type theories, th...
Abstract: Interest on runtime verification has grown in recent years and a lot of work has been focused on finding suitable formal...
Abstract: Program Validation (testing) and Verification (formal proof) are too often seen as disjoint subject areas. We observe th...
Abstract: For a long time, the arguments that members of the cryptographic community used to exhibit in favor of the security of c...
Abstract: The technique of partial order reduction (POR) for probabilistic model checking prunes the state space of the model so t...
Abstract: In this talk I will present the first principles of dynamic tracing, in particular tracing of systems programs. Tracing ...
Abstract: Abstract interpretation is a technique which has allowed the development of very powerful program analyzers and transfor...
Abstract: I will be talking about two main topics. First, on Privacy in Location-aware Services: supplying location-aware services...
Abstract: Several types of parallelism can be exploited in logic programs while preserving correctness and “theoretical effi...
Abstract: Formal verification of imperative programs provides a high guarantee of software quality, but it is usually a human inte...
Abstract: Automatic Generation of Smart, Security-Aware GUI Model Abstract: In many software applications, users access applicatio...
Abstract: SecureUML is a modeling language for adding (role-based) access-control requirements to software-system models. SecureUM...
Abstract: We present a new algebraic semantics for constraint logic programming based on Freyd’s allegories. Our objectives ...
Abstract: Representing and handling state mutations in Prolog can be cumbersome without resorting to internal database, global var...
Abstract: Abstract machines provide a certain separation between platform-dependent and platform-independent concerns in compilati...
Abstract: Formalisms involving some degree of nondeterminism are frequent in computer science. In particular, various programming ...
Abstract: I will present a simple(!) categorical framework for Logic Programming that gives a syntax, and semantics for logic prog...
Abstract: While there are well-understood methods for detecting loops whose iterations are independent and parallelizing them, the...
Abstract: IMDEA Software has unique oportunities for students that want to get involved in research. The European Master in Comput...
Abstract: Model driven development holds the promise of reducing system development time and improving the quality of the resultin...
Abstract: Verification of multi-agent systems is a challenging task due to their dynamic nature, and the complex interactions betw...
Abstract: Since the mid-90’s, the automata techniques have been one of the dominant approaches to temporal verification. In ...
Abstract: I will briefly explain the basic concepts of functional programming. I will then move on to show you typical examples of...
