Defence of dissertation in the field of computer science, Olli Saarikivi, M.Sc. (Tech)

Automated reasoning boosts program analysis

Olli Saarikivi, M.Sc. (Tech) will defend the dissertation: "Symbolic Methods for Transducers and Testing" on 16 February 2018 at 12 noon at the Aalto University School of Science. In the dissertation, methods for analyzing program behavior based on automated reasoning were explored. Applications to improving the performance of stream transformations and to automating software testing are presented.

Programs receive inputs during their execution from, for example, users or other information systems. To reduce the chance of programs containing errors, they are tested by running them with many different inputs. However, it is typically not practical to test all inputs, as even small programs may have astronomically many input combinations. Additionally, many inputs will produce equivalent behavior and thus redundant tests. An alternative approach is to represent classes of program executions that have equivalent behavior as systems of equation where inputs appear as variables. Solving these systems of equations allows a testing tool to systematically generate inputs for non-redundant tests. Furthermore, there exist solvers for these kinds of systems of equations that use automated reasoning to efficiently arrive at a solution or proof that no solution exists.

In the disseratation, this approach is applied to testing multi-threaded programs, where, in addition to inputs, the way threads are scheduled affects the execution. An extension of the approach to software verification, which aims to prove the absence of errors in a program, is also studied and improved on. In a second line of research, similar approaches based on automated reasoning are applied to the problem of optimizing programs that perform stream transformations. The connections between software testing/verification and program optimization are discussed, as both these fields of research benefit from reasoning methods for the internal behavior of programs.

The presented software testing and verification tools achieve results that are competitive with those presented in previous work. The methods developed on optimizing stream transformations can offer significant speedups over traditional techniques and hand-optimization. This work also advances the state of the art in automata theory by providing the first minimization algorithm for a specific class of symbolic automata.

Dissertation release (pdf)
 

Opponent: Adjunct Professor Rupak Majumdar, Max Planck Institute for Software Systems, Saksa

Custos: Associate Professor Keijo Heljanko, Aalto University School of Science, Department of Computer Science

Electronic dissertation: http://urn.fi/URN:ISBN:978-952-60-7787-1