Functional Programming and Property-Based Testing

test loop

This is a mirror of the elective course 'SM2-TES: Functional Programming and Property-Based Testing' offered in the spring 2021 on the MSc education in Software Engineering at the Maersk Mc-Kinney Moller Institute, University of Southern Denmark.

Previous versions of the course were given in the spring of 2018, 2019, and 2020 at SDU and in January 2016 and 2017 as 02913: Advanced Analysis Techniques at DTU Compute, the Technical University of Denmark (DTU).

This course material is posted here for the purpose of information sharing. I don't believe in password-protected course administration systems. As a scholar I (continue to) benefit from freely available online material. This is a personal contribution to uphold such an eco-system.

Course content

The course is two-fold.

On the one hand it introduces functional programming: Immutable data, algebraic datatypes, pattern matching, recursion, functions as first-class values, proper tail calls, type-directed programming and functional programming patterns.

On the other hand it introduces 'Property-based testing' (QuickCheck) (next generation automated testing) expressed within the functional programming context: Generators, properties, shrinking, statistics of generators, type-directed testing, testing of imperative code while touching upon a number of more general testing concepts as debugging, unit-testing, corner cases, blackbox and whitebox testing and fuzzing.

Finally the course covers a number of real-world case studies of property-based testing, e.g., an automated test of the AUTOSAR specification for Volvo.


The course consists of a mix of lectures and practical exercises, held in weekly 4-hour sessions.

Lectures: Tuesdays 12:15-16:00 (+ Fridays 12-16) online over Zoom

Lecturer: Jan Midtgaard

Course material

For the OCaml introduction we will use Jason Hickey's "Introduction to Objective Caml".


Lecture Topic Material Notes and exercises
01 Installation, OCaml, QCheck, BNF grammars Hickey chap.1,2,3-3.1.1, lec01.pdf, grammar.pdf exercises
02 Recursive functions, tuples and lists, labeled and optional arguments, testing implication properties Hickey chap.3.1.2-3.3,4,5, lec02.pdf exercises
03 Algebraic data types, references, records, exceptions, generator composition, observing generators Hickey chap.6-6.4,6.6,7,8,9, lec03.pdf exercises
04 Modules, shrinking, and model-based testing of Patricia trees Hickey chap.11,12 (+ parts of chap.13), lec04.pdf, qc-model.pdf, Midtgaard: QuickChecking Patricia Trees exercises
05 Model-based testing of stateful code with a state-machine framework lec05.pdf, State-machine lecture note exercises
06 Case study: LevelDB + code in other languages, tail-calls, function generation, more on properties lec06.pdf, Norton: QuickCheck A Silver Bullet for testing? (QuickChecking Google's LevelDB), Wlaschin: Choosing properties for property-based testing exercises
07 Other frameworks, case study: Volvo/AUTOSAR, project ideas + details lec07.pdf, Hughes: Certifying your car with Erlang, Arts-al: Testing AUTOSAR software with QuickCheck exercises
08 Case study: computational geometry, coverage, program generation lec08.pdf, Sergey: Growing and Shrinking Polygons for Random Testing of Computational Geometry video, slides, paper exercises
09 Inference rules, Curry-Howard, program generation, and compiler testing lec09.pdf, Pałka-al: Testing an optimising compiler by generating random lambda terms, Wadler: Propositions as Types, Midtgaard-al: Effect-Driven QuickChecking of Compilers exercises
10 Race condition testing with parallel state machines, Stack-Driven Program Generation of WebAssembly, Integrated shrinking lec10.pdf, Hughes: Testing the Hard Stuff and Staying Sane, aplas20.pdf Jacob Stanley: Gens N'Roses - Appetite for Reduction exercises
11 Sanitizers and Fuzz Testing lec11.pdf, Sanitizers: ASan, MSan, UBSan, American Fuzzy Lop (AFL) homepage, QuickStart guide, README, technical details, libFuzzer, OSS-Fuzz exercises
12 Project presentations, final course evaluation, course summary lec12.pdf

Running QCheck from the toplevel

Running QCheck from utop

Building a QCheck test with ocamlbuild