Plans for 02913 "Advanced Analysis Techniques" (January 2017 - QuickChecking)


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

We will initially study and work with the basic concepts within the functional programming language OCaml (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

For the OCaml introduction we will use Jason Hickey's "Introduction to Objective Caml".
English/Danish dictionary of commonly used terms
OCaml installation instructions
Source code of minimal QCheck example, Windows note, also see screencasts below
QCheck API documentation
QCheck source code
Calling C from OCaml: Orig. FFI example, Ctypes example, explanation
Calling C++ from OCaml: example code, explanation


Day Topic Material Exercises
Mon 2/1 Intro: OCaml, QuickCheck. slides Hickey chap.1,2,3-3.2,4 Exercises 1
Tue 3/1 Tuples and lists, labeled and optional arguments,
classification. slides
Hickey chap.3.3 + 5
Claessen-Hughes:ICFP00 (-3.1)
Exercises 2
Wed 4/1 Algebraic data types + generators, shrinking, testing exception-throwing code. slides Hickey chap.6-6.4,6.6,7,8,9
Claessen-Hughes:ICFP00 (3.2-)
Exercises 3
Thu 5/1 OCaml's module system,
stateful testing with algebraic and model-based specifications. slides
Exercises 4
Fri 6/1 Case study: Growing and Shrinking Polygons for Random Testing of Computational Geometry video, slides
More on properties + project ideas. slides
Case study: QuickChecking Google's LevelDB slides
Sergey-ICFP16, code
Choosing properties for property-based testing
Bug report, testing code
Exercises 5
Mon 9/1 Project presentation: Quickchecking OCaml Compilers by Generating Lambda Terms
Project/exam formalities slides
Case study: Quickchecking Static Analysis Properties
Look at other frameworks
EDSL code
Exercises 6
Wikipedia's QuickCheck entry
QuickCheck in every language
Tue 10/1 Presentation of other frameworks slides,
Case study: Certifying your car with Erlang video
Guest lecture: Jesper Louis Andersen - Real World QuickCheck slides
Hypothesis (Python)
FsCheck (F#)
jsverify (JavaScript)
quickcheck (Prolog)
QuickCheck (Haskell)
Wed 11/1 (project work) - -
Thu 12/1 (project work) - -
Fri 13/1 (project work) - -
Mon 16/1 (project work) - -
Tue 17/1 (project work) - -
Wed 18/1 (project work) - -
Thu 19/1 Report handin (project work) - -
Fri 20/1 Project presentations - -

Running Kaputt from the toplevel

Building a Kaputt test with ocamlbuild