Typed Functional Programming and Software Correctness

Software testing has been an important, if not prevalent way of checking software correctness. In this article I will tell how have my doctoral dissertation on testing and verification of imperative software as well as my work experience after the studies led me to typed functional programming, which consequently gave me a different perspective on automatic software testing. Furthermore, I’ll explain why functional programming and static type systems are important for software correctness.

Continue reading

Almost There with Firehosing KLEE, First Debian Bug Reported

If C++ wasn’t a so beautiful programming language, I guess I would have been done with implementing support for Firehose in KLEE long time ago. This week I learned another nicety of C++, which is undefined static variable initialization order. In spite of it, I am mostly done with implementing Firehose in KLEE. Beside that, I reported a bug in the hostname tool, and I played with linking dependencies in the LLVM bitcode form with a program under analysis in KLEE. Continue reading

Putting KLEE to Test


A coding period of the Google Summer of Code 2016 program has started this Monday and I’m participating in the program with the Debian project by integrating KLEE into Debile. What is worth noting is that this nicely aligns with what I’ve been working on in my PhD program, namely symbolic execution of Debian software with KLEE. I named the project Clover.

While I already had something done for the project before GSoC’s coding period started, here is what I’ve done this week. I’ll try to have weeklies throughout the whole GSoC.

Continue reading

JPF-Doop is dead, long live JDoop!

JDoop source code

JDoop source code snippet

In my first year of a PhD program, I worked on a software testing technique that combines concolic (or dynamic symbolic) execution and feedback-directed random testing. An implementation followed and it was dubbed JPF-Doop. The name was trying to honor two tools that formed the foundation of JPF-Doop – on one hand, it was Java Pathfinder and to be more precise, it was JDart (back then JPF-JDart) that performs concolic execution, and on the other hand there was Randoop, which performs feedback-directed random testing. The name was a bit clumsy.

Continue reading

Presentation of JPF-Doop at FMCAD 2013

I am happy to say that I have my first document written as a PhD student and accepted by reviewers. It is a 2-page research summary titled “Automatic Testing of Software Libraries”. The venue where I will present it is the FMCAD 2013 Student Forum, taking place from the 20th to the 23rd of October this year in Portland, Oregon.

The summary is about research and a tool that we’ve been working on. The tool is JPF-Doop, and it is an integration of JPF-JDart and Randoop into a single tool. JPF-Doop is a tool for testing of Java libraries. JPF-Doop comprises feedback-directed random testing from Randoop and concolic execution from JPF-JDart. So far we have seen decent improvements in terms of code coverage compared to the baseline Randoop. Hopefully there will be a release of the tool very soon. I will also demo it at the FMCAD conference to anyone interested.

At the Student Forum I will give a short talk and have a poster. If you will be at this year’s FMCAD or at any of the collocated events – MEMOCODE, DIFTS, and HWMCC’13 – and you are interested in software testing and symbolic execution, it would be nice to have a chat.