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