Vague or "fuzzy" concepts appear almost everywhere. The combination of fuzzy logic with logic programming opens the possibility of having automated reasoning on fuzzy information and, subsequently, a big potential for real life applications. The talk will present some of my research on fuzzy logic programming. Starting with fairly simple examples, I will present the syntax and semantics of fuzzy Horn clauses, some theoretical results and the generalised multi-adjoint framework. A description of our tool (RFuzzy) and some of its applications complete the talk.

This is joint work with Susana Munoz

We present a declarative language with a formal semantics for specifying both users' privacy preferences and services' privacy policies. Expressiveness and applicability are maximized by keeping the vocabulary and semantics of service behaviours abstract. A privacy-compliant data-handling protocol for a network of communicating principals is described.

Contents: We give a short survey on the following topics on verification of multithreaded programs:

• SPIN
  • Specification in Promela
  • Saving space: COLLAPSE & automata encoding
  • Saving time: partial order reduction
• Modular verification for general programs
  • Owicki-Gries
  • Rely-guarantee
  • Thread-modular model checking
  • Multithreaded Cartesian abstraction
  • Concurrent procedures specification
  • Thread simpolfication
  • Cartesian abstraction refinement
• Modular verification for resources & locks
  • Owicki-Gries
  • Concurrent separation logic

The notion of approximate equivalence of programs plays a fundamental role in several fields of computer science. In particular one way of tackling this when dealing with probabilistic programs is to consider the statistical distance (SD) between memory distributions. Despite the SD being a well-known concept from measure theory, all the treatment it has received in the computer science literature to model and reason about approximate equivalence of programs has been very poor and deficient.

In this talk I will present an ongoing work that attempts to fill this gap. First I will show a SD-based extension of a relational Hoare logic for probabilistic programs proposed by Barthe et al that allows to reason about approximate observational equivalence. Second I will exhibit related results for two typical scenarios in the domain of cryptography: uptobad programs and the presence of adversaries of unknown code. To conclude, I will illustrate the benefits of this approach by showing how it allowed to formalize two case studies in the Certicrypt framework.

Zero-knowledge proofs are two-party interactive protocols where one party (the prover) convinces the other one (the verifier) that it knows some secret value, without leaking anything about this secret. ZK proofs have a vast applicability in the domain of cryptography, stemming from the fact that they can be used to force potentially malicious parties to abide by the rules of a protocol, without forcing them to reveal their secrets. In this talk I will a give an intuitive introduction to interactive ZK proofs and describe in more detail a class of three-round ZK proofs, known as Sigma-protocols. I will show how Sigma-protocols can be formalized as probabilistic programs in the CertiCrypt framework---built on top of the Coq proof assistant---and how mechanized programming language techniques can be used to formally prove that a protocol is complete (a honest prover always convinces a verifier), sound (a dishonest prover can only convince a verifier with negligible probability) and perfect zero-knowledge (a verifier does not gain any secret information from participating in the protocol). I will also show how a large class of ZK proofs can be seen as instances of a generic Sigma-protocol, for which soundness, completeness and zero-knowledge can be established once and for all. I will conclude by describing a means of combining ZK proofs to obtain proofs of more complex formulae using the AND and OR Boolean operators.

Relational program logics allow reasoning about two programs or two runs of the same program. They provide an elegant means to prove correctness of compiler optimizations or equivalence between two implementations of an abstract data type, and a unifying formalism for specifying and verifying properties like non-interference or determinism. Yet the current technology for relational verification remains underdeveloped. We provide an abstract theory of product programs that supports a direct reduction of relational verification to standard verification. We illustrate the benefits of our method with a state-of-the-art optimization for incremental computation, and with standard examples of loop optimizations. All examples have been verified using the Why framework for program verification.

In this talk I will try to present the main notions of the work through examples without going into many technical details.

In this talk we present a MySQL code generator for OCL expressions which is based on the use of stored procedures for mapping OCL iterators. Our code generator is defined recursively over the structure of OCL expressions. We discuss the class of OCL expressions covered by our definition (which includes, possibly nested, iterator expressions) as well as some extensions needed to cover the full OCL language. We also discuss the efficiency of the MySQL code produced by our code generator, and compare it with other results on evaluating OCL expressions on medium-large scenarios. Our motivation here is two-fold. On the one hand, our code gen- erator addresses the problem of evaluating OCL expressions on really large scenarios: instead of having to "load" them in memory (a time-consuming, or even impractical task for OCL evaluators), we can (i) store these scenarios in a database, (ii) apply our code generator to the expressions to be evaluated, and (iii) execute the resulting query statements on the database. On the other hand, our code generator provides a key component for any models-to-code development process, where the source models include OCL expressions and the target code evaluates these expressions on relational databases. We have implemented our code generator in the MySQL4OCL tool. A brief demo of this tool will also be shown.

Implementors of abstract machines face complex, and often interacting, decisions regarding, e.g., data representation, instruction design, instruction encoding, or instruction specialization levels. These decisions affect the performance of the emulator and the size of the bytecode programs in ways that are often difficult to foresee. Furthermore, studying different alternatives by implementing abstract machine variants is a time-consuming and error-prone task because of the level of complexity and optimization of competitive implementations, which makes them generally difficult to understand, maintain, and modify. This also makes it hard to generate specific implementations for particular purposes.

I will show a systematic approach to the automatic generation of implementations of abstract machines which is aimed at harnessing some of these difficulties, where different parts of the abstract machine definition (e.g., the instruction set or the internal data and bytecode representation) are specified separately and automatically assembled in the code generation process.

Alternative versions of the abstract machine are therefore easier to produce, and variants of their implementation can be created mechanically. This even allows generating implementations tailored to a particular context.

"Shared resources" is the term we use to refer to the notation and companion methodology used to teach concurrent programming at undergraduate level in our university for the last 15 years.

Originally conceived as a gentle extension of a formal notation for teaching abstract data types -- just adding the extra synchronization component -- they have recently proved useful out of the classroom to model and analyze complex, real world systems.

From the point of view of software design, shared resources can be used to fill a gap in widely used modeling notations regarding concurrency. At the code level, they have been used for semi-automatic generation of correct-by-construction code. Finally, wrt. analysis and validation, they can be seen as automata generators.

The talk will introduce the formalism from the different points of view mentioned above, and will present current and future research lines. If time permits, the talk will include a short demo on the use of shared resources and model checking for validation of concurrency requirements.

This is joint work with Manuel Carro, Angel Herranz and Juanjo Moreno-Navarro.

Side-channel attacks break cryptosystems by exploiting information that is revealed by the system's implementation, e.g. through time or power consumption. Research on countermeasures against side-channel attacks has so far focussed either on (1) cryptographic primitives that remain secure despite leaky implementations, or on (2) hardening implementations, e.g. through program transformations that hide variations in the execution time. In this talk, I will show how one can achieve provable security against timing attacks by combining guarantees from the cryptographic primitive with guarantees from the implementation. This hybrid approach is considerably simpler and more efficient than purely cryptographic or purely implementation-based solutions, making it an interesting topic for further investigation. I will end with a discussion of/invitation to future work.

I introduce subsequence invariants, a new class of invariants for the specification and verification of concurrent systems. Unlike state invariants, which refer to the state variables of the system, subsequence invariants characterize the behavior of a concurrent system in terms of the occurrences of sequences of synchronization events.

Subsequence invariants satisfy an interesting combination of properties: They are compositional in the sense that a system inherits all the invariants of its constituent processes; they can be computed in polynomial time; and they can still express interesting system properties. The mathematics behind subsequence invariants are interesting in their own right and suggest some promising extensions to the existing theory.

Separating data into lock-protected resources is an established paradigm of multi-threaded programming. Programs following that paradigm are verified by approaches that are typically rooted in a verification method of Owicki and Gries. For any such approach there are properties whose proof is only feasible if the user provides good auxiliary variables. What properties can be proven without the burden of inventing auxiliary variables? We partially describe the set of such properties by showing (a) the absence of exact characterization in terms of abstract interpretation, (b) a nontrivial superset, containing properties that can be proven by abstract interpretation with a form of Cartesian abstraction, and (c) a nontrivial subset, containing properties that can be proven by abstract interpretation with another form of Cartesian abstraction.