Automated Software Engineering

Given the progress in computing science, it is somewhat puzzling that software development still requires so much manual labor. Developer effort is wasted on writing tests, fixing bugs and optimizing code, rather than focusing on creating new innovative ideas and products. There are many approaches to automating some of the tedious tasks in software engineering, so we focus here on just a couple of specific topics.

NB! Learning to use a bounded model checker or symbolic execution engine is a high-priority skill for our lab. We are willing to provide scholarship to students willing to master this technique.

Symbolic Log Generation

Log files can be used to analyze a system. There are automated methods that to mine these and extract important information from log files. There are also program analysis techniques, bounded model checking and symbolic execution, that can traverse a program's source code and visit all possible branches in the source code. This can be used (e.g., by Visual Studio's IntelliTest) to generate input that will reach every branch. The task for this thesis is to take an open source tool, such as Java Pathfinder or JBMC, and adapt this to generate log files.

Test Generation for Programming Courses

Assume you have a "correct" solution to a programming assignment. We would like to automatically generate test cases to check that student submissions return the same results. First, it would be nice to have a simple tool that just takes a list of inputs together with a template for the unit tests and then generates the assertions with the result obtained from the reference implementation. Then, it would be nice to experiment with different approaches to automating test input generation, including symbolic execution and combinatorial testing.

Automated feedback generation using program synthesis

Program synthesis can be used to provide students with high quality feedback and hints about what is wrong in their program. Sumit Gulwani describes the method as follows: "The underlying technique involves exploring the space of all candidate programs, applying teacher-provided rewrite rules to the student’s incorrect program, to synthesize a candidate program equivalent to the reference solution while requiring a minimum number of corrections." The goal of this thesis is to implement the ideas of this paper to produce a feedback tool for Java (using JSketch) and try this approach for some of our own programming assignments.