Plans for 02913 ”Advanced Analysis Techniques” (January 2017 – QuickChecking)

·       The course 02913 on “Advanced Analysis Techniques” takes place at DTU starting Monday, January 2nd at 9.00 and lasts for three weeks.

·       Location: (to be determined)

·       The topic for January 2017 is QuickChecking

·       It is organized by Jan Midtgaard, Flemming Nielson and Hanne Riis Nielson.

·       To sign up for the course you should register at CampusNet or contact the organizers.

·       For formalities please take a look at


The need to test software is as relevant as ever, witness the massive amount of programs that surround us (mobile apps, web servers and services, automotive software, infrastructure such as the Danish Rejsekort, etc.). Testing either of these (either module-by-module or as a whole) can however be both cumbersome and tricky to exercise all the possible execution paths. QuickCheck (also known as randomized property- based testing) offers an alternative testing approach, in which the developer tests properties (specifications) across a range of arbitrary generated inputs. As such, the technique can exercise a piece of software on a bigger fraction of the input space and on cases a human would potentially forget or omit. In doing so, QuickCheck can find counterexamples to a given specification which can help a developer to fix any encountered problems and ultimately produce more robust software. For this reason the approach has gained increasing acceptance within the software industry, initially within the Erlang programming language community (a language used by Ericsson) and more recently it has been used for testing AUTOSAR components for Volvo cars.

Course content

This course provides an introduction to randomized property-based testing exemplified by QuickCheck. We will study

·      properties (what specification should hold for a given piece of software?)

·      generators (techniques for generating arbitrary input, from simple ones to more complex ones)

·      shrinking techniques (for reducing counterexamples down to something humanly comprehensible)

·      statistics (for studying the distribution of the generators' output)

·      techniques for testing both stateless and stateful programs

·      case studies using QuickCheck from both academia and industry

We will initially study and work with the basic concepts within the functional programming language OCaml (and the course will provide an introduction to this language).
 In personal projects students are requested to QuickCheck a piece of software, to write a report summarizing their results, and to deliver an oral presentation to all course attendees.

Course material and time schedule

·      Available on CampusNet.