Formal Methods Division Retreat – Lysekil 2019
23 – 24 May 2019, at Strandflickornas Havshotell in Lysekil, Sweden.The FM retreat on 23–24 May is now booked. There will be 21 people attending the event, with the first day also open to guests from other divisions.
Venue
We will be staying at Strandflickornas Havshotell in Lysekil:
There are some spa/sauna facilities at the hotel. Don’t forget to bring swimwear if you’re planning to use these!
The meeting room has a projector with a HDMI interface (bring your own adapter) as well as a flip chart.
Travel
A bus will pick us up from Chalmers in the morning on Thursday, 23 May, at 7:30am sharp. The bus will leave from “Kopparbunkern” (the climbing gym at campus, next to our building) on Thursday, and will (most likely) return us to Järntorget, which is the location of the CSE summer party which takes place in the evening of Friday, 24 May.
If you are only attending the first day and want to return to Gothenburg using public transport, the closest bus stop is Havets hus (280m from the hotel). Bus 841 will take you all the way to downtown Gothenburg.
Dinner
On recommendation, we will dine at Märtas Mat. They will prepare a set 3-course dinner for us, using what’s in season and fresh for the day (they have been notified about your dietary restrictions).
Sea Kayaking
Make sure to bring an extra set of outdoor/sports clothing (e.g. a thin windproof jacket).
Program
Preliminary schedule
Thursday 23 May
Friday 24 May
| Time | Activity |
|---|---|
| 07:30 | Breakfast |
| 09:00 | |
| 11:00 | Break |
| 11:15 | Workshop: Experience outside the box |
| 11:45 | Break |
| 12:00 | Lunch |
| 13:00 | Session 6 (3x20min, chair: Wolfgang) |
| Hanaa: Designing privacy aware software systems | |
| Quentin: Efficient functional priority queues | |
| Thomas: Binary Correctness and Applications for OS Software | |
| 14:00 | Break |
| 14:15 | Session 7: Division meeting (50min) |
| 15:00 | Break |
| 15:30 | Bus returns to GBG |
Talk Abstracts
Trends in AI and Theorem Proving
by Moa Johansson
Combining machine learning and reasoning is an emerging trend in AI research. I recently attended the AITP (AI in theorem proving) conference and spotted some interesting topics.
Automating Higher-Order Logic
by Simon Robillard
This talk will give an overview of the different techniques and tool used in automated theorem proving for higher-order logic, including the latest developments in HO-SMT solving and the extension of superposition to HOL.
New Project on Verified Cyber Physical Systems
by Magnus Myreen
In September this year, Hira Syeda from Data61 Australia will join our Formal Methods division as a new postdoc. She will work on a new WASP Expedition Project on construction of verified cyber physical systems.
In this short talk, I’ll introduce the topic of the WASP Expedition Project and outline what the Chalmers side (Hira and I) will contribute to the project.
The project is a collaboration between Chalmers and KTH. David Broman is the co-PI at KTH. Elias Castegren (from Uppsala) is David Broman’s postdoc on the project.
We can work it out - Personal perspectives on software verification
by Wolfgang Ahrendt
In the light of a new composition of the FM group, I want to give a selective overview of my research profile, highlighting topics where I anticipate connections to other people in the group.
Binary Correctness and Applications for OS Software
by Thomas Sewell
Computer software is usually written in one language (the source language) and translated from there into the native binary language of the machine which will execute it. Most operating systems, for instance, are written in C and translated by a C compiler. If the correctness of the computer program is important, we must also consider the correctness of the translation from source to binary.
In the first part of this talk, I will introduce the SydTV tool which validates the translation of low-level software from C to binary. In the specific case of the seL4 verified OS software, this validation combines with the existing verification to produce a trusted binary.
The time taken to execute a program is normally considered to be a property of the final binary rather than the source code. Some programs have essential timing constraints, which ought to be checked by some kind of analysis. In the second part of this talk, I will show how the SydTV translation analysis can be reused to support a timing analysis on the seL4 binary. This design permits the timing analysis to make use of type information from the source language, as well as specific guidance provided at the source level by the kernel developers.
Designing privacy aware software systems
by Hanaa Alshareef
As the General Data Protection Regulation (GDPR) within the European Union came into effect, designing privacy preserving systems is becoming a necessity for practitioners. There are many technical challenges that accompany GDPR compliance. In context of system design, verifying that an architectural design is compliant with the regulations can be a hard task for engineers. Providing a privacy aware system which guarantees that an architectural design embodies regulation-oriented principles such as the right to be forgotten, or collecting and disclosing based on individual’s consent, address that challenge for engineers.
Concurrency Theory and Collective Behaviour
by Yehia Abd Alrahman
In this talk I will briefly discuss the concept of collective behaviour from a concurrency point of view. I will mainly explain my understanding of how a collective behaviour can be designed in terms of interactions among different components. Thus, I will abstract from the continuous behaviour of individual components and will focus on the discrete nature of interactions.
Namely, I will try to answer the following questions:
- What is a collective behaviour?
- Why the design of a collective behaviour is challenging?
- What do we need to be able to design a collective behaviour?
My Research Interests: Past, Present and Future
by Gerardo Schneider
A very high-level overview about my research interests over time, with a wish list on what I would like to do in the future.
Synthesis From Temporal Specifications
by Nir Piterman
In this give the background for the idea of synthesis, the automatic production of designs from their temporal logic specifications. We are interested in reactive systems, systems that continuously interact with other programs, users, or their environment and specifications in linear temporal logic. Classical solutions to synthesis use either two player games or tree automata. I will give a short introduction to the technique of using two player games for synthesis. If time permits, I will talk about some of newer results and how people are using this kind of synthesis in practice.
Verification of an interactive theorem prover for HOL
by Oskar Abrahamsson
This talk will be about my work towards a verified implementation of an interactive theorem prover for higher-order logic. The theorem prover I am building is based on HOL Light which is implemented in the LCF-style. I will talk about: (i) what it means for a theorem prover to be LCF-style; (ii) what has been done towards the new theorem prover; and (iii) what needs to be done.
Reasoning upon security of the Cloud via Description Logics
by Claudia Cauli
Description Logics are, for the most part, a family of decidable fragments of First Order Logic; descending from knowledge representation formalisms and database systems, but also being close relatives of modal logics. Thanks to their model-theoretic semantics, practical decision procedures have been developed to solve inference problems such as: consistency, subsumption, entailment, instance retrieval, and query answering; all reducible to knowledge base satisfiability. In my research, I aim to use Description Logics to model, verify, and reason upon security of Cloud services. The impact of such an application could be substantial in software development as it might aid the automation of security tasks - such as threat modelling and risk assessment - that are difficult to be done without the expertise of a security engineer. Many “hows” have to be answered here: How could DLs be exploited to model the Cloud? How could DLs be made expressive enough to give a faithful depiction of the Cloud and precise answers when queried? How could modelling via DLs be used to express, infer, and identify vulnerabilities to security threats?
Efficient functional priority queues
by Quentin Ladeveze
This presentation will focus on two functional implementations of priority queues. Based on an analogy with a specific representation of integers, the first implementation can support the insert operation in constant time. The second implementation bootstraps the first one to allow us to find the minimal element of a queue and to merge two queues in constant time.
A type-system for Transient Information-Flow Control
by Marco Vassena
Recently discovered attacks like Spectre, Meltdown and Foreshadow rely on transient (speculative and out-of-order) execution to exfiltrate sensitive data through microarchitectural side-channels. Even though several hardware and software mitigations have been proposed and deployed, the subtleties of transient execution require a formal approach to reason about their security guarantees. To this end, we apply techniques from Information-Flow Control to study effective countermeasures against transient execution attacks. In this on-going work, we formalize transient execution for a while-language with linear memory and arrays and design a type-system for transient information-flow control.
Proof-guided quantifier instantiation for SMT
by Koen Claessen
SMT-solvers solve problems by working with underapproximations (expressed in SAT) that are successively strengthened during proof search. This technique works well for specific theories such as equality, numbers, and arrays, but has worked less well for more general concepts such as full first-order quantification. In this talk, I report on my ongoing work of using overapproximations (which are also expressed in SAT) and successive weakening during proof search instead! This results in a proof-guided abstraction refinement for computing relevant instances of quantifiers in an SMT-setting. Initial results show that the new method greatly outperforms existing heuristics and methods for quantifier instantiation in SMT-solvers, at least for pure first-order problems with only quantification and no extra theories.
Neural network verification
by Sólrún Einarsdóttir
As neural networks have gained popularity due to their effectiveness in performing diverse tasks, and found applications in safety-critical systems such as autonomous vehicles, there is a growing demand for safety guarantees about their behavior. I will describe some recent approaches to verification of neural networks and possible next steps.
Hardware development in HOL4 for verified stacks
by Andreas Lööw
I will say talk about proof-producing Verilog code generator that can translate HOL circuit to Verilog circuits. I will also present a verified processor developed with the help of this code generator, and how we with the help of the verified CakeML compiler have built verified computer systems (so called verified stacks) based on this processor. If there is time, I will also mention future research plans.
DPella: A programming framework for differential privacy with accuracy
by Alejandro Russo
Differential privacy offers a formal framework for reasoning about privacy and accuracy of computations on private data. It also offers a rich set of building blocks for constructing data analyses. When carefully calibrated, these analyses simultaneously guarantee privacy of the individuals contributing their data and accuracy of their results for inferring useful properties about the population. One important building block for differential privacy are composition theorems, which allow multiple differentially private data analyses to be composed together with a graceful degradation of the privacy and accuracy parameters. The compositional nature of differential privacy has motivated the design and implementation of several programming languages aimed at helping a data analyst in programming differentially private data analyses. However, most of the programming languages for differential privacy proposed so far provide support for reasoning about privacy but not for reasoning about accuracy of data analyses. To overcome this limitation, in this work we present DPella, a programming framework providing data analysts with support for reasoning about privacy, accuracy and their trade-offs. DPella is implemented as a domain specific language in the functional programming language Haskell. The distinguished feature of DPella is a novel component which statically tracks the accuracy of different data analyses. In order to make tighter accuracy estimations, this component leverages information-flow control techniques, in the form of taint analysis, for automatically inferring statistical independence of the different noise quantities added for guaranteeing privacy. We show the flexibility of our approach by implementing classical counting queries (e.g., CDFs) found in the literature and how DPella exposes the trade-offs between privacy and accuracy. Furthermore, we use DPella to analyze hierarchical counting queries (like those done by Census Bureaus), where accuracy have different constrains per level and data analysts should figure out the best manner to trade-off privacy to meet the accuracy requirements.
This is a work-in-progress in collaboration with Elisabet Lobo Vesga, Marco Gaboardi and Gilles Barthe.
Formal Biochemistry
by Sandro Stucki
To biologists, Chemical Reaction Networsk (CRNs) and Rule-Based Models (RBMs) are formalisms for describing biochemical systems. To computer scientists, they are instead known as Petri Nets and Graph Transformation Systems (GTSs). In this talk, I will show how these simple and elegant formalisms can be used to model biochemical processes and, more generally, combinatorially complex stochastic processes with a dynamic network structure. If time permits, I’ll present some preliminary work on geometrically enhanced RBMs and the automated generation of rate-equations and ODEs tracking higher-order statistics from a large class of rule-based systems.
Workshop: Experience outside the box
lead by Sandro Stucki
A workshop by and for FM:ers about experiences collected outside our primary research activities. Have you always wanted or learn more about popular science communication, cross-disciplinary collaborations, AI, bird watching, improvisational theater, or single malt whiskey? Well, you might not be alone. Let’s share our experiences and brainstorm project ideas outside the FM-box.
Add your topics to the word cloud at https://www.menti.com/9my3pdheh5(closed)- Click here to see the results
Pair introductions
Each speaker will be introduced by another speaker according to the table below.
At the beginning of the meeting, there will be 15 minutes reserved for interviews. For each pair of speakers (A and B),
- in the first half of the 15 min, speaker A interviews speaker B;
- in the second half of the 15 min, speaker B interviews speaker A.
Later, before A is gives their talk, B introduces A; and vice versa.
The interviewer is to ask questions that provide material for the introduction. We recommend taking some notes and trying to find something fun / previously unknown / interesting to say about the interviewee.
The introductions should be only 1–2 minutes long, but the whole process of interviewing and introducing others is meant to be an (awkward but) interesting way to get to know each other.
| A (introduces B) | B (introduces A) |
|---|---|
| Alejandro Russo | Oskar Abrahamsson |
| Gerardo Schneider | Marco Vassena |
| Koen Claessen | Andreas Lööw |
| Magnus Myreen | Sólrún Halla Einarsdóttir |
| Moa Johansson | Claudia Cauli |
| Nir Piterman | Hanaa Alshareef |
| Thomas Sewell | Simon Robillard |
| Wolfgang Ahrendt | Quentin Ladeveze |
| Yehia Abd Alrahman | Sandro Stucki |