In this thesis, we have defined a symbolic execution technique to automatically generate test suites for programs written in functional programming languages that can find the behavioural differences between a reference implementation and a set of potentially different implementations. Our symbolic execution technique uses a constraint solver in order to find a model that satisfies all constraints that together represent an execution path through the program. Furthermore, our technique utilises manually defined budget constraints to guide the symbolic execution to more interesting areas of the programs. These budget constraints define an initial budget that dictates when the symbolic execution terminates, and a set of costs associated to certain operations such as calling (specific) functions or performing (specific) pattern matches. This allows the symbolic execution to deplete budgets faster when it explores functions or branches of a program that are deemed "unlikely to be interesting". This results in less system resources being used on exploring these uninteresting execution paths, and instead allows for exploration of deeper paths in more interesting areas of the programs. Our budget constraint optimisation strategy works alongside other well-known optimisation strategies for symbolic execution such as early branch pruning and reusing intermediate results, more commonly known in the field of symbolic execution as compositioning.

In order to perform our symbolic execution on functional programs, we have defined a variation of Control Flow Graphs (CFG) for functional programming languages which allow modelling the execution flow between the different expressions that form the body of functions in functional programming. Additionally, our technique uses a constraint solver in order to find what paths through the program are feasible and to generate inputs that will lead to the execution of said paths. To allow us to specify these constraints on a higher-level, we have defined an intermediate Domain Specific Language (DSL), which can be transformed into a lower-level language understood by the constraint solver. We refer to this DSL as our Intermediate Constraint Language (ICL). Our ICL supports working seamlessly with type systems that allow inheritance, rather than only supporting Algebraic Data Types (ADT).

Furthermore, we have developed a symbolic execution engine for programs written in a pure and functional subset of the Scala programming language. This symbolic execution engine implements our proposed symbolic execution technique alongside the other described optimisation techniques. We have used this implementation in order to measure the effectiveness of our symbolic execution technique. In order to do this, we have used our technique in a scenario to automatically generate test suites for real student submissions of introductory assignments to functional programming. We have performed a comparison between the obtained branch coverages and mutation scores with our technique and the manually written test suites that have been used for multiple years. Finally, we have reflected on the feasibility of using this approach in practice by looking at the execution time and the number of inquiries to the constraint solver, required to generate test suites that are able to find an adequate number of errors. ... Read more

For this project, JEM-id tasked us with creating a proof of concept of a new online auction in the form of a web application for Royal FloraHolland. JEM-id is a software company operating in the agricultural domain.
The pre-existing digital auction is not available as a web application and has generated technical debt over the past twenty years of it is existence.

The main challenge of the project was to make sure the application is capable of sufficiently handling the current load of the auction while maintaining similar performance. This translates to a stable connection with a ping of fewer than 30 milliseconds for clients within the Netherlands.
On top of that, the system had to be scalable to support higher numbers of buyers in the future.
We used a microservice architecture able to balance the load over several servers to resolve this.
We spread the load of communicating with clients to services separate from the main application service.
This allowed the main application service to solely and adequately keep track of the state of the clock and determine the winner of a session.

To validate that we indeed achieved the main goals of the project, we created a simulation that would simulate any number of clients connecting to the clock auction and placing bids.
In this process, we generated buyer and auctioneer behaviour by analysing transaction data. We extracted several distributions from the data and sampled from it to make it more realistic.
In the end, we ran this simulation ten times for chunks of an auction with 610 connected clients.
A few peaks showed up where pings from client to server were significantly higher than usual. However, in the long run, the system showed low standard deviations in ping, meaning the general consistency was high.
Overall, the results we gathered showed that our application was able to deal with 610 connected clients.

In the end, we consider our project to be a success.
First of all, we showed that a clock application in the browser can be implemented with seven weeks of development time.
Secondly, we showed that such an application could handle a realistic amount of traffic without much trouble, given sufficient computing resources.
These two accomplishments show that replacing the current clock application with a web-based application is feasible. ... Read more