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