This is a joint work with Ekaterina Komendantskaya.
First-order logic programming traditionally relies on SLD-resolution, in which termination of derivations is crucial for deciding entailment, whereas the exact proof content of derivations may be opaque. In Coalgebraic Logic Programming (CoALP), derivations can proceed infinitely (or corecursively), as long as intermediate proof structures can be finitely observed. We propose a type-theoretic semantics for this new kind of structural resolution. We formalize several derivation strategies possible in logic programming (SLD-resolution, resolution by term-matching, structural resolution), and show that they are sound w.r.t. the type system we propose. We also establish an exact formal relation between structural resolution and SLD-resolution within this typed framework.

Smart-cards are seen as one of the most secure, tamper-proof, and trusted devices for implementing confidential operations, such as secure log-in, for financial, communication, security and data management purposes.
These operations typically involve communication between smart-cards and third-party systems. Such communication must be secure, and developers usually prefer proprietary implementations which create the illusion of security as hide the card's code.
In this talk we will present REPROVE, a first-order based system that reverse-engineers the communication trace and deduces the card's functionalities. REPROVE does not require access to the card, and deals with both inter-industry and proprietary implementations.

This is a joint work with Jean-Frédéric Etienne, Florent Anseaume and Véronique Delebarre from SafeRiver which we will present at ICSE SEIP 2015.
We report on our industrial experience in using formal methods for the analysis of safety-critical systems developed in a model-based design framework. We first highlight the formal proof workflow devised for the verification and validation of embedded systems developed in Matlab/Simulink. In particular, we show that there is a need to: determine the compatibility of the model to be analysed with the proof engine; establish whether the model facilitates proof convergence or when optimisation is required; and avoid over-specification when specifying the hypotheses constraining the inputs of the model during analysis. We also stress on the importance of having a certain harness over the proof activity and present a set of tools we developed to achieve this purpose. Finally, we give a list of best practices, methods and any necessary tools aiming at guaranteeing the validity of the verification results obtained.