Replacing Store Buffers by Load Buffers in Total Store Ordering
Parosh Aziz Abdulla, Uppsala University, Sweden
   
Abstract: We consider the verification of concurrent programs running under the classical TSO (Total Store Order) memory model. The model allows write to read relaxation corresponding to the addition of an unbounded store buffer (that contains pending store operations) between each processor and the main memory. In this talk, we introduce a novel semantics which we call the dual TSO semantics that replaces each store buffer with a load buffer that contains pending load operations. The flow of information is reversed, i.e., store operations are performed by the processes atomically on the main memory, while values of variables are propagated from the memory to the load buffers of the processes. We show that the two semantics are equivalent in the sense that a program will reach identical sets of states when running under the two semantics. Furthermore, we present a simple and effective reachability algorithm for checking safety properties of programs running under the dual semantics.
Short Bio: Parosh Aziz Abdulla is a professor at the department of information technology, Uppsala University. His areas of interest include formal methods, automata theory and logic in computer science, program verification and model checking. He has more than 150 publications, and has received more than 10 best paper awards including ones from the European association for software science and technology at ETAPS 2013, the European association for theoretical computer science at ETAPS 2010 and ICALP 2001, and the European association for programming languages and systems at ETAPS 2000. He was a co-recipient of the LICS test-of-time award in 2016, for his paper in 1996 on the verification of well quasi-ordered programs. In 2017, he was a co-recipient of the CAV award for his contributions in the area of verification of programs with infinite state spaces.
Slides

Fault injection, from software to hardware and reversed
Axel Legay, Inria Rennes, France
   
Abstract: Fault injection is a well known method to test the robustness and security vulnerabilities of software. Fault injections can be explored by simulations (cheap but not validated) and hardware experiments (true, but very expensive). Recent simulation works have started to apply formal methods to the detection, analysis, and prevention of fault injection attacks to address verifiability. However, these approaches are ad-hoc and extremely limited in architecture, fault model, and breadth of application. Further, there is very limited connection between simulation results and hardware experiments. Recent work has started to consider broad spectrum simulation approaches that can cover many fault models and relatively large programs. Similarly the connection between these broad spectrum simulations and hardware experiments is being validated to bridge the gap between the two approaches. This presentation highlights the latest developments in applying formal methods to fault injection vulnerability detection, and validating software and hardware results with one another.
Short Bio: Axel Legay is a researcher at the Institut national de recherche en informatique et en automatique (INRIA Rennes, France). He received his Ph.D. in Computer Science from the University of Liège, Belgium. His main research interests are in formal verification and cyber security. He is a major contributor of statistical model checking which he recently used for fault-injection analysis. Axel is also a referee for top journals and conferences. He has organized several international conferences such as ATVA, TACAS, or RV.
Slides

Automated Black-box verification of Networking Systems
Alexandra Silva, University College London, UK
   
Abstract: Our society is increasingly reliant on complex networking systems, consisting of several components that operate in a distributed/concurrent fashion, exchange data that may be highly sensitive, and are implemented with a mix of open and closed-source code. In this talk, we will present a broad overview of techniques and tools to automate the modelling and verification of networking software systems. We will focus mainly on the model learning paradigm, originally proposed in artificial intelligence, to automatically build an automaton model of a running system in a black-box fashion -- purely via interactions with the running system.
Short Bio: Alexandra Silva is a theoretical computer scientist whose main research focuses on semantics of programming languages and modular development of algorithms for computational models. A lot of her work uses the unifying perspective offered by coalgebra, a mathematical framework established in the last decades. Alexandra is currently a senior lecturer at University College London. Previously, she was an assistant professor in Nijmegen and a post-doc at Cornell University, with Prof. Dexter Kozen, and a PhD student at the Dutch national research center for Mathematics and Computer Science (CWI), under the supervision of Prof. Jan Rutten and Dr. Marcello Bonsangue. She was the recipient of the Presburger Award 2017, the Leverhulme prize 2016, and an ERC starting Grant in 2015.
Slides