SICSA M&A: Scottish Theorem Proving Meeting

Date(s) - 13/03/2015
1:15 pm - 5:00 pm

Heriot-Watt University, Postgraduate Centre


Room PG 2.02
Postgraduate Centre (map)
Heriot-Watt University (direction)


If you would like to give a talk, please contact Manuel Maarek.

1.15 – 2.00 pm Lunch
2.00 – 2.40 pm Peng Fu (University of Dundee) Horn-formulas as Types for Structural Resolution
2.40 – 2.50 pm Discussion
2.50 – 3.30 pm Andriana Gkaniatsou (University of Edinburgh) Logging-in Insecurely: Reverse-Engineering the Smart-Card Communication Layer
3.30 – 3.40 pm Discussion
3.40 – 4.10 pm Coffee Break
4.10 – 4.50 pm Manuel Maarek (Heriot-Watt University) Improving Predictability, Efficiency and Trust of Model-Based Proof Activity
4.50 – 5.00 pm Discussion
5.00 pm Close


Horn-formulas as Types for Structural Resolution
Peng Fu (University of Dundee)
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.

Logging-in Insecurely: Reverse-Engineering the Smart-Card Communication Layer
Andriana Gkaniatsou (University of Edinburgh)

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.

Improving Predictability, Efficiency and Trust of Model-Based Proof Activity
Manuel Maarek (Heriot-Watt University)

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.

This entry was posted in .