SASUF Workshop 2019

Workshop “Making systems trustworthy by model checking and symbolic execution”

Tuesday, May 7, University of Stellenbosch

Committee Room A521, 5th floor, Main Engineering Building

Schedule

08.45 – 09.00	Introductions
09.00 – 09.30	An Overview of Recent Progress in Stateless Model Checking
09.30 – 10.00	Multi-agent systems
10.00 – 10.30	Java Pathfinder and some of its applications
10.30 – 11.00	Break
11.00 – 11.30	Concolic Testing of Higher-order Functional Languages
11.30 – 12.00	A day at the beach: From Java PathFinder to COASTAL
12.00 – 12.30	Searching Fast and Slow: Fuzzing and Symbolic Execution
12.30 – 14.00	Lunch
14.00 – 14.30	Systematic Generation of Programs with Guaranteed Syntax Errors
14.30 – 15.00	An Empirical Comparison of Systematic and Random Grammar-based Fuzzing
15.00 – 15.30	Break
15.30 – 16.00	SMT Result Caching for Symbolic Execution
16.00 – 16.30	Symbolic Automata Learning
16.30 – 17.30	Closing
19.00 - …	Dinner at Hussar Grill

Speakers and topics

Willem Visser (University of Stellenbosch): Searching Fast and Slow: Fuzzing and Symbolic Execution

Abstract: </br> The past few years a number of research groups built tools where they combined fuzzing and symbolic execution, and in this talk we will discuss yet another case. The combination of these two technologies for bug finding is a no-brainer: fuzzing covers lots of cases with very little effort, but can get stuck generating inputs to highly constrained behaviours, for which symbolic execution is good. What makes our approach (COASTAL) somewhat unique is that it uses concolic execution rather than classic symbolic execution and that the fuzzer and the concolic execution were built into the same framework, from scratch (in other words it is not two existing tools that are being combined). In this talk we will discuss the design decisions, the integrated architecture and show some examples.

Cyrille Artho (KTH Royal Institute of Technology): Java Pathfinder and some of its applications

Abstract: </br> This talk gives an overview of Java Pathfinder and then presents the case study "Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder". That work analyzes a Java model of the priority inheritance protocol for mutual exclusion, as implemented in the RTEMS open-source real-time operating system. We verified this model using Java Pathfinder to detect potential data races, deadlocks, and priority inversions. JPF detected a known bug in the RTEMS implementation, which we modified along with the Java model. Verification of the modified model showed the absence of data races, deadlocks, and established nine protocol-specific correctness properties.

Moeketsi Raselimo (University of Stellenbosch): An Empirical Comparison of Systematic and Random Grammar-based Fuzzing

Bernd Fischer (University of Stellenbosch): Systematic Generation of Programs with Guaranteed Syntax Errors

Kostis Sagonas (Uppsala University): An Overview of Recent Progress in Stateless Model Checking

Abstract: </br> A successful technique for finding concurrency bugs (i.e., defects that arise only under some thread schedulings) and for verifying their absence is stateless model checking (SMC). Given a terminating program, which may be annotated with assertions, SMC systematically explores the set of all thread schedulings that are possible during runs of this program. A special runtime scheduler drives the SMC exploration by making decisions on scheduling whenever such choices may affect the interaction between threads. Given enough time, the exploration covers all possible executions and detects any unexpected program results, program crashes, or assertion violations. The technique is entirely automatic, has no false positives, does not consume excessive memory, and can quickly reproduce the concurrency bugs it detects. SMC faces the problem that the number of possible thread schedulings grows exponentially with the length of program execution, and must therefore be equipped with techniques to reduce the number of explored executions. This talk will overview algorithms and tools for stateless model checking, focusing on recent progress in algorithms for dynamic partial order reduction (DPOR), both under Sequential Consistency and Weak Memory Models.

Kostis Sagonas (Uppsala University): Concolic Testing of Higher-order Functional Languages

Abstract: </br> Concolic testing is a fully automatic software testing technique that combines concrete and symbolic execution of a program unit in an attempt to explore all the code paths in this unit or at least explore all its paths up to a depth bound. In this talk, we will describe how concolic testing can be applicable to high-level languages in general and to functional programming languages in particular. For such languages, the concolic engine needs to efficiently support pattern matching, recursive data types such as lists, recursion and higher-order functions. We will also briefly talk about the engineering effort that concolic testing tools require, in particular in interfacing with SMT solvers.
The talk will also include a demo of CutEr (as in “more cute”), a concolic testing tool for Erlang, and will briefly report on some of the bugs in the implementation of Erlang/OTP that CutEr has discovered and the coverage that it manages to achieve.

Jaco Geldenhuys (University of Stellenbosch): A day at the beach: From Java PathFinder to COASTAL

Stefan Gruner and Nils Timm (University of Pretoria): Multi-agent systems

Jan Taljaard (University of Stellenbosch): SMT Result Caching for Symbolic Execution

Phillip van Heerden (University of Stellenbosch): Symbolic Automata Learning