Tuesday, May 7, University of Stellenbosch
Committee Room A521, 5th floor, Main Engineering Building
Use Google Maps for directions.
| 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 |
Willem Visser (University of Stellenbosch): Searching Fast and Slow: Fuzzing and Symbolic Execution
Abstract: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: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: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: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.