This year, SEFM is happy to feature the following two high-class keynote speakers.
We Need a Formal Semantics for Testability Transformation; SEFM community to the rescue?
Mark Harman | Engineering Manager, Facebook London, and Professor of Software Engineering, University College London.
Testability transformation transforms a program, while preserving test adequacy according to some test adequacy criterion. The goal is to ease test data generation according to the adequacy criterion. Although test adequacy criteria are relatively well-defined, the semantics preserved by testability transformation has never been formally defined, nor properly theoretically investigated. Nevertheless, testability transformation provides many opportunities to dramatically improve the efficiency and effectiveness of software testing. There is, therefore, a pressing need for an underpinning formal semantics for testability transformation. In this talk, I will briefly describe automated test design at Facebook, before moving on to outline the open problem of testability transformation semantics, hoping to stimulate the Software Engineering and Formal Methods community to take up this challenge.
This talk covers joint work with Sapienz automated testing team at Facebook.
Hunting Resource Manipulation Bugs in Linux Kernel Code
Andrzej Wasowski | Professor of Software Engineering, IT University of Copenhagen
Software projects suffer from conceptually simple resource manipulation bugs, such as accessing a deallocated memory region, or acquiring a non-reentrant lock twice. The VBDB bug database contains entries for 100 such real bugs from several open source projects, including the Linux Kernel project. These historical bugs have been collected with the aim of giving concrete well understood and documented cases to program analysis researchers, in order to boost program verification research. I will discuss simplicity and complexity of real software manipulation bugs on examples selected from VBDB.
One way to reduce the amount of such bugs is to use code scanners such as Smatch or Coccinelle. Unfortunately, while very efficient, code scanners are typically based on syntactic pattern matching, which is insufficient for identifying problems that span multiple functions and involve dynamically allocated memory. We have developed a shape-and-effect inference system for C that constructs a lightweight semantic abstraction, more analyzable than syntax. A model checker is then used to match semantic bug patterns over the control flow graph decorated with the shape-and-effect abstractions.
Experiments run with our prototype analyzer (EBA) shows better precision and effectiveness than with syntactic bug scanners. We have been so far able to identify 10 previously unknown locking bugs in the Linux kernel. The bugs are confirmed as real by the Kernel developers, and five of them have been already fixed in response to our reports. I will conclude, sketching how we combine EBA with another tool, RECONFIGURATOR, to massively scan Linux kernel code for bugs in atypical source configurations.