AI4FM / 2015

Colocated with AVoCS'15, Edinburgh, Scotland, 1st September 2015

The AI4FM 2015 workshop will be held in the ICMS building in the historic old town of Edinburgh (see venue info below the programme).


  • From 9:00: Registration
  • 9:25: Welcome: AI4FM 2015Alan Bundy - University of Edinburgh - Slides
  • 9:30: Invited talk: The Role of Human Creativity in Mechanized VerificationJ Strother Moore - University of Texas at Austin - Abstract - Slides
    Abstract: When people solve a challenging problem they often "polish" the solution to make it easier to understand and communicate. This happens in all technical fields but in this talk I focus on its occurrence in formal verification, largely by way of an example problem solved interactively with students in one of my classes. Examples from industrial applications of formal methods include revisions to models to eliminate unnecessary complexity, revisions to variable orderings to shorten state space exploration, and the process by which a key inductively provable lemma was discovered. I claim that while this natural urge to polish is important to publication it is detrimental to progress: how do we automate the creative steps in verification?
  • 10:30: Coffee
  • 11:00: Event-B and Cloud ProversAlexei Iliasov, Paulius Stankaitis, and David Adjepon-Yamoah - Newcastle University - Abstract - Slides
    Abstract: We discuss the whys and hows of remotely managing a collection of automated theorem provers supporting verification of Event-B models in the Rodin Platform. We report on the current state of the work, our general aspirations and a range of technical obstacles encountered so far.
  • 11:30: First-Order Logic for the Analysis of Programs on Weak Memory ModelsAlexei Lisitsa - The University of Liverpool - Abstract - Slides
    Abstract: In this paper we present the applications of automated reasoning for classical first-order logic for the analysis of safety properties of programs running on weak memory models. The reachability within a program state space is modelled by derivability in first-order logic, and the safety verification is reduced to the refutation of a first-order formula, which is then tackled by a generic finite model finder. We present a detailed case study and report on further experimental evidence of the feasibility of the approach.
  • 12:00: Nuprl's Inductive Logical FormsMark Bickford, Robert L. Constable, Rich Eaton, and Vincent Rahli - Cornell University - Abstract - Slides
    Abstract: For more than a decade, we have been working on specifying, verifying, and synthesizing asynchronous distributed protocols using the Nuprl proof assistant. Only recently we have been able to do so for complicated protocols such as Paxos. This has been made possible thanks to the level of abstraction of our specification language called the Logic of Events (LoE). This paper discusses our main automation tool, namely our Inductive Logical Forms (ILFs), which are first order formulas that characterize the responses of a system to events in terms of observations made at causally prior events.
  • 12:30: Lunch
  • 13:30: VERIFOLIO: A Portfolio for Software VerificationYulia Demyanova, Thomas Pani, Helmut Veith, and Florian Zuleger - Vienna University of Technology - Abstract - Slides
    Abstract: In recent work, we study empirical metrics for software source code, which can predict the performance of verification tools on specific types of software. Our metrics comprise variable usage patterns, loop patterns, as well as indicators of control-flow complexity and are extracted by simple data-flow analyses. We demonstrate that our metrics are powerful enough to devise a machine-learning based portfolio solver for software verification. We show that this portfolio solver would be the (hypothetical) overall winner of both the 2014 and 2015 International Competition on Software Verification (SV-COMP). This gives strong empirical evidence for the predictive power of our metrics and demonstrates the viability of portfolio solvers for software verification.
  • 14:00: Learning and Exploration in Automated Theorem ProvingMoa Johansson - Chalmers University of Technology - Abstract - Slides
    Abstract: This note describes a new project with the purpose of combining the advantages of statistical machine learning with those of symbolic methods for lemma discovery, such as theory exploration. We can thus better exploit the resources in large electronic proof libraries to gain heuristic knowledge to, for example, create more efficient lemma discovery techniques or provide hints as to which induction scheme to try in an automated prover.
  • 14:30: Scaling Automated Theory ExplorationChris Warburton and Ekaterina Komendantskaya - University of Dundee - Abstract - Slides
    Abstract: We investigate the theory exploration (TE) paradigm for computer-assisted Mathematics and identify limitations and improvements for current approaches. Unlike the theorem-proving paradigm, which requires user-provided conjectures, TE performs an open-ended search for theorems satisfying given criteria. We see promise in TE for identifying new abstractions and connections in libraries of software and proofs, but realising this potential requires more scalable algorithms than presently used.
  • 15:00: Coffee
  • 15:30: Compact Explanations of Why Malware is BadWei Chen, Charles Sutton, Andrew D. Gordon, David Aspinall, Igor Muttik, and Qi Shen - University of Edinburgh (and others) - Abstract - Slides

    Abstract: Researchers and malware analysts have identified hundreds and thousands of mobile applications as malware. These malware instances are organised into families based on some common unexpected behaviours, e.g., sending premium messages, accessing locations, and intercepting incoming messages and calls, etc. However, except some unclear online technical descriptions of several famous malware families, to the best of our knowledge, people have no idea of what exactly happens in mobile malware or what kind of behaviour of a mobile application makes it bad. This brings a challenging research problem: to automatically generate compact and precise explanations of unexpected behaviours in a mobile application if it has been identified as malware.

    This research has several potential benefits, including: help people get better understanding of potential threats hidden in mobile applications; provide hints for malware analysts before more expensive investigation; support automatic generation of malware analysis reports; and provide clear and friendly references for security policy designers, etc.

    Some fundamental technical questions we will answer are as follows. How could we characterise and formalise an application's behaviour as efficiently and precisely as possible? What kind of behaviour is unexpected with respect to a specific application and how to figure it out automatically? Once a certain behaviour has been identified as unexpected, how could we automatically generate an explanation of this behaviour and in what kind of form? Finally, how could we evaluate generated explanations?

  • 16:00: Typed Meta-interpretive Learning for Proof StrategiesColin Farquhar, Gudmund Grov, Andrew Cropper, Stephen Muggleton, and Alan Bundy - Heriot-Watt University (and others) - Abstract - Slides
    Abstract: Formal verification is increasingly used in industry. A popular technique is interactive theorem proving, used for instance by Intel in HOL light. The ability to learn and re-apply proof strategies from a small set of proofs would significantly increase the productivity of these systems, and make them more cost-effective to use. Previous learning attempts have had limited success, which we believe is a result of missing key goal properties in the strategies. Capturing such properties will require predicate invention, and the only technique we are familiar which supports this is meta-interpretive learning (MIL). We show that MIL is applicable to this problem, but that without type information it offers limited improvements in quality over previous work. We then extend MIL with types and give preliminary results indicating that this extension learns better-quality strategies with suitable goal properties.
  • 16:15: Tinker: A Graph Based Proof Strategy System (demo)Pierre Le Bras, Yuhui Lin, and Gudmund Grov - Heriot-Watt University - Abstract - Tinker website
    Abstract: Tinker is a tool for designing and evaluating proof strategies based on proof-strategy graphs (PSGraphs). Here, we represent proof strategies as open-graphs, which are directed graphs with additional input/output edges. Tactics appear as nodes in a graph, and can be 'piped' together by adding edges between them. Goals are added to the input edges of such a graph, and flow through the graph as the strategy is evaluated. Properties of the edges ensure that only the right 'type' of goals are accepted. The tool currently works with the Isabelle and ProofPower theorem provers, while we are working on integrating it with Rodin. In this paper, we will demo new features of the Tinker tool, with a focus on debugging in the GUI.
  • 16:30: Discussion: The Future of the AI4FM Workshop
  • 17:00: Closing

Proceedings

The extended abstracts of all talks have been compiled into the preliminary proceedings, which can be downloaded here. The proceedings will be published as a Newcastle University technical report shortly.

Venue

The AI4FM 2015 workshop will be held in the headquarters of the International Centre for Mathematical Sciences (ICMS), which is at 15 South College Street, Edinburgh, EH8 9AA. All talks will take place in the Newhaven Lecture Theatre on Level 4 of the building. The main ICMS Reception is located on Level 3.

Coffee/tea and lunch breaks

Refreshments and lunch will be available during the designated breaks. Lunch will be served in the Chapterhouse on Level 1.

Getting to the venue

The easiest way to access the ICMS building is via the A7 (South Bridge/Nicholson Street). The entry for South College Street is between the Old College of the University of Edinburgh and the Edinburgh Arts and Picture Framers shop (opposite the Black Medicine coffee shop). The ICMS building will be half way along South College Street, on your left. There will be a blackboard at the entry labelled with AVoCS/AI4FM. For more information see the AVOCS website.

AI4FM 2015 starts at 9:25 on Tuesday 1 September. Registration will be open from 9:00 so that you can collect your name badge and welcome pack. Once you have entered the ICMS building you will need to press the ICMS button to get access to the venue. Once you have entered the venue, please follow the signs for the registration.