Scottish Theorem Proving Seminar

Celebrating 20 years of Scottish Theorem Proving seminars in Scotland and
60 years of Computing in Glasgow

Glasgow, 19 May 2017


Eventbrite - SICSA sponsored event: Scottish Theorem Proving Seminar 2017

About STP seminars

The Scottish Theorem Proving Seminar Series provide a common and friendly venue for communication and sharing of recent work on theorem proving and related forms of formal verification.

View more »

Venue and Date

Venue: Room SAWB 423, Sir Alwyn Williams Building
School of Computing Science, University of Glasgow
18 Lilybank Gardens, Glasgow, G12 8RZ
Date: 19 May 2017, starting from 13:15 with lunch

View programme »

Organisers and Sponsors

Chairs: Oana Andrei (University of Glasgow) and Alice Miller (University of Glasgow)
Sponsors: SICSA, School of Computing Science and 60th anniversary of Computing in Glasgow

View more »

About STP

Theorem proving research is notably strong in Scottish universities, with active groups and researchers in at least six departments. The Scottish Theorem Proving Seminar Series provide a common venue for communication and sharing of ideas by all these researchers. At least once a year, one of the departments hosts an informal seminar for the whole Scottish theorem proving community. As well as theorem proving, other related fields are also represented, e.g. model checking and other forms of formal verification. This is a friendly venue for PhD students and RAs to discuss their work in progress and get feedback. The usual format is to have three or four talks in an afternoon session, starting around 14:00 and finishing by 17:00. Lunch will be provided from 13:15 and later in the afternoon there will be cake during the coffee break.

This year we celebrate 20 years of Scottish Theorem Proving seminars (over 40 events). Therefore it is a great opportunity for the School of Computing Science to host the first seminar of 2017 to join the on-going celebration of the 60th anniversary of the School at the University of Glasgow.

Attending the seminar, the lunch and the coffee break with celebratory cake are free (thanks to our sponsors!). In order to help with catering arrangements, please register at our Eventbrite page.

Programme

13:15 - 14:00 Lunch
14:00 - 14:40 Tom Melham (University of Oxford), Effective Validation of Low-Level Firmware (Invited talk)
14:40 - 15:20 Yue Li (Heriot-Watt University), Productive Corecursion in Logic Programming
15:20 - 15:40 Coffee break
15:40 - 16:20 Chris Warburton (University of Dundee), Quantitative Benchmarks for Theory Exploration
16:20 - 17:00 Oana Andrei (University of Glasgow), Statistical Machine Learning and Probabilistic Model Checking for Interactive Systems

Abstracts

  • Effective Validation of Low-Level Firmware, Tom Melham:
    Today’s microelectronics industry is increasingly confronted with the challenge of developing and validating software that closely interacts with hardware. These interactions make it difficult to design and validate the hardware and software separately; instead, a verifiable co-design is required that takes them into account. We demonstrate a new approach to co-validation of hardware/software interfaces by formal, symbolic co-execution of an executable hardware model combined with the software that interacts with it. We illustrate and evaluate our technique on three realistic benchmarks in which software I/O is subject to hardware-specific protocol rules: a real-time clock, a temperature sensor on an I2C bus, and an Ethernet MAC. We provide experimental results that show our approach is both feasible as a bug-finding technique and scales to handle a significant degree of concurrency in the combined hardware/software model.
  • Productive Corecursion in Logic Programming, Yue Li:
    Logic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/coinductive soundness of formulae is a challenging task. For example, the existing state-of-the-art algorithms can only semi-decide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental and important undecidable property is productivity. If a derivation is infinite and coinductively sound, we may ask whether the computed answer it determines actually computes an infinite formula. If it does, the infinite computation is productive. This intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing. Recently, an algorithm was presented that semi-decides a weaker property — of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this talk I will strengthen these recent results. I will propose a method that semi-decides productivity of individual derivations for regular formulae. Thus I will give an algorithmic counterpart to the notion of productivity of derivations in logic programming. This is the first algorithmic solution to the problem since it was raised more than 30 years ago. I will also present an implementation of this algorithm.
  • Quantitative Benchmarks for Theory Exploration, Chris Warburton:
    Automated theory exploration has the potential to help scientists, mathematicians and programmers discover unexpected properties of their models, theories and programs; but has so far been limited to small-scale experiments, with only a few, hand-picked, data points. We address this problem by re-purposing existing benchmarks from the theorem proving domain, producing an order of magnitude more data for evaluation, and use it to evaluate the performance of a state of the art exploration system. To combat the long run times of these systems, we also propose a pre-processing method to identify promising subsets of a theory, sacrificing completeness to gain speed. It is our hope that the availability of robust evaluation methods, and scalable algorithms, will encourage competition and innovation, making theory exploration more useful and relevant as a formal methods tool.
  • Statistical Machine Learning and Probabilistic Model Checking for Interactive Systems, Oana Andrei:
    Formal methods are traditionally used to specify and analyse the intended behaviour of software systems, while statistical methods are traditionally used to analyse logged data from instrumented systems. We show how to bring the two methods together to analyse how users actually interact with an instrumented interactive system. We use statistical machine learning to generate probabilistic formal models of interactive systems usage from logged data. Statistical machine learning is employed not to learn a predictive model, but to encapsulate the behaviour of a given data set, from actual deployments, in a formal model that is amenable to temporal logic analysis. We then analyse the generated formal models by probabilistic model checking. The results of the analyses inform evaluations of system design, or might, for example, provide feedback to developers or motivate system redesign. We illustrate by application to logged data from a deployed mobile application used by hundreds of users.

Sponsors

We are grateful to SICSA for their generous support of the STP seminar, as well as the Chairs of the 60th celebrations at the School of Computing Science, University of Glasgow.