Scottish Theorem Proving Seminar

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.

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.