INDUSTRY DAY
At the Industry Day, contributions of Formal Methods from the practice will be presented.
Industry representatives will demonstrate the use of Formal Methods using suitable tools.
Accepted Papers
| Paper | Authors |
| Shifting Left for Early Detection of Machine-Learning Bugs | Liblit, Luo, Molina, Mukherjee, Patterson, Piskachev, Schäf, Tripp, Visser |
| Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks | Hashemi, Kretinsky, Rieder, Schmidt |
| Backdoor Mitigation in Deep Neural Networks via Strategic Retraining | Dhonthi, Hahn, Hashemi |
| veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System | Amir, Freund, Katz, Mandelbaum, Refaeli |
| Shifting Left: Opportunities and Techniques for Early Verification in Model-Based Design | Canny, Rajhans, Sticksel |
| Specification-Guided Critical Scenario Identification for Automated Driving | Molin, Aguilar, Nickovic, Zhu, Bemporad, Esen |
| A Systematic Approach to Automotive Security | Ebrahimi, Marksteiner, Nickovic, Bloem, Schögler, Eisner, Sprung, Schober, Chlup, Schmittner, König |
| Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny | Cassez, Fuller, Ghale, Pearce, Anton Quiles |
DOCTORAL SYMPOSIUM
A Doctoral Symposium will be held in conjunction with the 25th International Symposium on Formal Methods (FM 2023), 6-10 March. FM 2023 is hosted by the University of Lübeck.
Day
6 March 2023
Goals and Scope
This symposium aims to provide a supportive environment in which selected PhD students can present and discuss their ongoing work, meet other students working in the field of formal methods, and receive feedback and advice from experienced researchers. In addition to talks followed by discussions, the event will also provide opportunities for PhD students to meet senior academics in smaller groupings, to informally discuss research strategies, career aspects, or any other topic of interest.
If you are a PhD student researching any topic that falls within the area of formal methods, you are warmly invited to submit a Research Abstract for consideration to be selected as a participant of the Doctoral Symposium.
There will be a best presentation award.
Invited Speaker
Paula Herber, University of Münster
Important Dates
- Submission open: 21 November 2022
- Submission deadline: 01 December 2022
- Notification: 20 December 2022
Research Abstracts
Research Abstracts should be no more than 4 pages in Springer LNCS format. Your Research Abstract should:
- Outline the problem being addressed, its relevance, the solution you are working on, your research approach (such as your research method) and your expected contribution.
- Contain a very brief literature survey indicating the most important references related to:
- the problem being addressed and/or
- existing solutions as appropriate.
- Indicate your progress to date and the current stage of research.
The Research Abstract should be written by yourself as sole author, but may include references to relevant papers you have already published, including joint publications with collaborators.
How to Submit
Please upload your Research Abstract via the submission page.
Programme
Doctoral Symposium Chairs
- Wolfgang Ahrendt, Chalmers University of Technology, Gothenburg, Sweden
- Ralf Möller, University of Luebeck, Germany
Programme Committee
| Sebastian | Berndt | berndt@tcs.uni-luebeck.de | University of Luebeck |
| Mattias | Ulbrich | ulbrich@kit.edu | KIT (Karlsruhe Institute of Technology) |
| Rosemary | Monahan | Rosemary.Monahan@nuim.ie | Maynooth University |
| Sylvia | Melzer | sylvia.melzer@uni-hamburg.de | University of Luebeck |
| Eva | Darulova | eva.darulova@it.uu.se | Uppsala University |
| Van Den Bos | Petra | p.vandenbos@utwente.nl | University of Twente |
| Carlo | Furia | furiac@usi.ch | Università della Svizzera italiana |
| Max | Bannach | bannach@tcs.uni-luebeck.de | University of Luebeck |
D-CON 2023
The D-Con was founded as a forum of German researchers on Concurrency Theory to meet, collaborate, and exchange ideas. It became the yearly meeting of the GI Fachgruppe on Concurrency Theory, but is open to researcher from all over the world.
One of its main tasks is to connect the younger researchers in the field. Therefore, the meeting consists of several talks mostly from younger scientists that can talk about their research agenda, new ideas on ongoing work, or recent research results. The programme is enhanced with talks and tutorials from experienced researchers as wel as invited talks.
Dates
March 09 and 10 (ends after lunch)
Persons
Roland Meyer, TU Braunschweig
Kirstin Peters, Universität Augsburg
Invited Speaker
Heike Wehrheim, Universität Oldenburg
Klaus von Gleissenthall, Vrije Universiteit Amsterdam
Dinner
Wednesday, March 08, 19:30: Kartoffel-Keller (https://www.kartoffel-keller.de/); Please order before 19:45.
Thursday, March 09, 19:30: Schiffergesellschaft (https://schiffergesellschaft.de/)
Programme
Thursday, March 09:
| 09:00 – 10:00 | Heike Wehrheim Invited Talk | View-based semantics and logics for weak memory On modern multi-core architectures the behaviour of concurrent programs differs from the usually assumed sequential consistency (SC): the semantics is influenced by the underlying weak memory model. Unlike SC, threads might see different values for shared locations. In this talk, I will discuss semantics for concurrent programs on weak memory models characterised by such views of threads. Based on these semantics, I will then present a proof calculus for reasoning about concurrent programs. It follows the style of Owicki-Gries proof calculi (including interference-freedom checks), but employs a novel assertion language and novel Hoare triples for primitive commands. |
| 10:00 – 10:30 | Lara Bargmann | View-Based Axiomatic Reasoning for PSO Weak memory models describe the semantics of concurrent programs on modern multi-core architectures. Reasoning techniques for concurrent programs, like Owicki-Gries-style proof calculi, have to be based on such a semantics, and hence need to be freshly developed for every new memory model. Recently, a more uniform approach to reasoning has been proposed which builds correctness proofs on the basis of a number of core axioms. This allows to prove program correctness independent of memory models, and transfers proofs to specific memory models by showing these to instantiate all axioms required in a proof. The axiomatisation is built on the notion of thread views as first class elements in the semantics. In this talk, we investigate the applicability of this form of axiomatic reasoning to the Partial Store Order (PSO) memory model. As the standard semantics for PSO is not based on views, we first of all provide a view-based semantics for PSO and prove it to coincide with the standard semantics. We then show the new view-based semantics to satisfy all but one axiom. The missing axiom refers to message-passing (MP) abilities of memory models, which PSO does not guarantee. As a consequence, only proofs without usage of the MP axiom are transferable to PSO. We illustrate the reasoning technique by proving correctness of a litmus test employing a fence to ensure message passing. |
| 10:30 – 11:00 | Coffee Break | |
| 11:00 – 11:30 | Anton Opaterny | nekton: a linearizability proof checker Nekton is a tool for checking linearizability proofs of concurrent search structures. The tool is parametric in its heap abstraction, which also enables it to check proofs of inductive properties of graph structures. Hindsight arguments allow future-dependent linearization points. I describe the tool and give an example of a checked proof. |
| 11:30 – 12:00 | Jingyi Mei | Model Checking Quantum Continuous-Time Markov Chains Quantum computing technology may soon make revolutionary improvements in algorithm performance thus verification methods are necessary to improve the trustworthiness of quantum software. In this talk, we introduce the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties of QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-the-art real root isolation algorithm under Schanuel’s conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. |
| 12:00 – 12:30 | Felix Freiberger | Model Checking Concurrent Programs for Autograding in pseuCo Book With concurrent systems being prevalent in our modern world, concurrent programming is now a cornerstone of most computer science curricula. A wealth of platforms and tools are available for assisting students in learning concepts of concurrency. Among these is pseuCo, a light-weight programming language featuring both message passing and shared memory concurrency. It is supported by pseuCo Book, an interactive textbook, focusing on the theoretical foundations of pseuCo, concurrency theory. In this paper, we extend pseuCo Book with a chapter on Programming with pseuCo. At its core is a custom verification system, based on pseuCo’s Petri net semantics, enabling practical programming exercises to offer fast in-browser model checking that can validate the program’s internal use of concurrency features and provide comprehensive debugging features if a fault is detected. |
| 12:30 – 13:50 | Lunch | |
| 13:50 – 14:20 | Philipp Czerner | Making IP = PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms We show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasoning tools. Theoretically, interactive protocols exist for all PSPACE problems. The verifier of a protocol checks the prover’s answer to a problem instance in polynomial time, with polynomially many bits of communication, and with exponentially small probability of error. (The prover may need exponential time.) Existing interactive protocols are not used in practice because their provers use naive algorithms, inefficient even for small instances, that are incompatible with practical implementations of automated reasoning. We bridge the gap between theory and practice by means of a novel interactive protocol whose prover uses BDDs. We consider the problem of counting the number of assignments to a QBF instance (#CP), which has a natural BDD-based algorithm. We give an interactive protocol for #CP whose prover is implemented on top of an extended BDD library. The prover has only a linear overhead in computation time over the natural algorithm. We have implemented our protocol in blic, a certifying tool for #CP. Experiments on standard QBF benchmarks show that blic is competitive with state-of-the-art QBF-solvers. The run time of the verifier is negligible. While loss of absolute certainty can be concerning, the error probability in our experiments is at most 10^{-10}. |
| 14:20 – 15:10 | Christoph Ohrem | Deciding Asynchronous Hyperproperties for Recursive Programs We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same complexity of the model checking problem for finite state models. Beyond this, we study the model checking problem of our logic for pushdown models. We argue that the combination of asynchronicity and a non-regular model class studied in this paper constitutes the first suitable approach for hyperproperty model checking against recursive programs. |
| 15:10 – 15:40 | Roman Lakenbrink | Model Checking Dynamic Pushdown Networks with Communication Dynamic Pushdown Networks have been introduced as a model for multithreaded programs with recursion and dynamic thread creation. In this presentation, I will enrich this model by the possibility of communication between different threads via queues. I will consider the MSO Model Checking problem for this model and show how it can be decided approximately using graphs with bounded split-width. |
| 15:40 – 16:00 | Coffee Break | |
| 16:00 – 16:30 | Jens Oliver-Gutsfeld | Temporal Logics with language Parameters We study a systematic mechanism to enrich the traditional logics LTL, CTL^+ and CTL^* with the expressive power of different formal language classes and study the resulting expressive power as well as the satisfiability and model checking problems for a certain set of language classes. |
| 16:30 – 17:00 | Roland Guttenberg | Geometry of Reachability Sets of Vector Addition Systems Vector Addition Systems (VAS), aka Petri nets, are a popular model of concurrency. The reachability set of a VAS is the set of configurations reachable from the initial configuration. Leroux has studied the geometric properties of VAS reachability sets, and used them to derive decision procedures for important analysis problems. In this paper we continue the geometric study of reachability sets. We show that every reachability set admits a finite decomposition into disjoint almost-hybridlinear sets enjoying nice geometric properties. Further, we prove that the decomposition of the reachability set of a given VAS is effectively computable. As a corollary, we derive a simple algorithm for deciding semilinearity of VAS reachability sets, the first one since Hauschildt’s 1990 algorithm. As a second corollary, we prove that the complement of a reachability set always contains an infinite linear set. |
| 17:00 – 17:30 | Rebecca Bernemann | Hidden Markov Models with Unobservable Transitions We consider Hidden Markov Models (HMMs) that admit unobservable ε-transitions (also called null transitions), allowing state changes of which the observer is unaware. In particular we present an algorithm for determining the most probable explanation given an observation (a generalization of the Viterbi algorithm for HMMs) and a method for parameter learning that adapts the probabilities of a given model based on an observation (a generalization of the Baum-Welch algorithm). The latter algorithm guarantees that the given observation has a higher (or equal) probability after adjustment of the parameters and its correctness can be derived directly from the so-called EM algorithm. |
| 17:30 – 18:00 | Karla Messing | Hennessy Milner Theorems via Galois Connections A general and compositional framework that allows us to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (Hennessy-Milner theorems), which is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand. It covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. |
| 18:00 – 18:30 | Ira Fesefeldt | Putting Probabilities into Concurrent Separation Logic We develop a verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combined two kinds of separation logic — Quantitative Separation Logic and Concurrent Separation Logic — into a new separation logic that enables reasoning about lower bounds of the probability to realise a postcondition by executing such a program. Current research now also asks: 1) can we also reason about expected values in this logic and 2) can this logic also be implemented in a proof assistant? |
Friday, March 10:
| 09:00 – 10:00 | Klaus von Gleissenthall Invited Talk | VERIFYING SECURITY ACROSS HARDWARE & SOFTWARE Side-channel leaks via timing, cache, and speculation can expose sensitive information across traditional isolation barriers, putting our data at risk. Unfortunately, despite decades-long attempts at eliminating these leaks, new attacks are discovered by the day. Fundamentally, this is due to the following mismatch: Today’s hardware is extremely complicated because of its myriad fast paths and performance optimizations, yet, we reason about it based on coarse, implicit, and inaccurate models. This divide between model and reality results in leaks that fail to keep our data safe. In this talk, I will discuss my recent work on bridging the gap between model and reality. I will discuss recent work on proving that hardware is free of timing side-channels, how to make the verification task simpler for non-experts, and how to move towards more expressive leakage models. |
| 10:00 – 10:30 | René Pascal Maseli | Memory-model-aware scheduling for Bounded Model Checking Fine-grained Concurrency is notoriously hard for software developers due to the large number of interleavings. This complexity also applies to its verification, in particular due to optimizations performed by the underlying hardware introducing additional and rather unexpected behavior. Dartagnan is a Bounded Model Checker that accepts both a program and a description of the hardware architecture (TSO, ARM, PowerPC, etc.). To counteract the unexpected behavior, we introduce a notion of scheduling parametric in this architecture. This can be understood as guiding the search to interesting executions. |
| 10:30 – 11:00 | Coffee Break | |
| 11:00 – 11:30 | Jan Grünke | Tableaux for Reasoning about Axiomatic Memory Models CAT is a domain-specific language for the axiomatic definition of weak memory models. The syntax of the CAT language consists essentially of the formulation of constraints for binary relations. In doing so, derived relations can be defined for a program using the operations of binary relations. Then the set of consistent program executions can be constrained by acyclicity constraints over the defined relations. A lot of manual work has gone into proving properties of existing memory models. Therefore, it would be nice to have a method to automatically prove properties of memory models defined in CAT. For example, one goal is to decide for two given CAT specifications whether the first model is contained in the second. However, this problem is undecidable for the full syntax of CAT due to the presence of the complement operator. Therefore, we consider the monotone relational fragment of CAT without recursion but with transitive closure. In this talk, we focus on a tableau-based approach to deciding this fragment. For this purpose, we define a suitable normal form for relational terms and present a syntax-oriented circular tableau procedure based on it. |
| 11:30 – 12:20 | Jan Bookmann | Towards data-driven synthesis of approximate class invariants In object-oriented programming, the behavior of a method depends on the argument values provided as input and the internal state of the invoked object. Defensive programming practices require developers to perform input validation, which makes assumptions about argument values explicit. For example, the method argument „index“ for retrieving the n-th element stored in a list data structure must be greater than or equal to zero and less than its size. In contrast, the class invariant, which is maintained throughout the lifetime of an object, is often left implicit, even though it is crucial for program comprehension and verification. For example, the said size attribute is implicitly guaranteed to be always greater than or equal to zero. This talk reviews existing approaches to assertion inference and reports on our ongoing work to dynamically synthesize approximate class invariants from a class definition. Our data-driven approach draws inspiration from search-based program testing, symbolic execution and fuzzing to automatically construct objects that satisfy/violate the implicit class invariant. Combining this with techniques from inductive synthesis allows for the generation of an approximate class invariant through incremental refinements. |
| 12:20 – 12:30 | Business-Meeting | |
| 12:30 – 14:00 | Lunch (Business-Meeting) |