ENCODING CONSTRAINED LINKEDLISTS IN CBMC FOR A TESTING DSL

Sammanfattning

This thesis explores the use of bounded model checking for use in unit tests involving singularlylinked lists. Unit testing usually makes use of a known input and a known output to verifythat code functions correctly. Unit tests are however entirely inadequate to prove the correctnessof code. Bounded model checking can however prove the correctness of code up to a certainbound by symbolic reasoning about the code instead of executing it. Bounded model checkingis however largely inaccessible non-experts. The rUnit project explore the unification of theseseparate approaches by creating a framework for the bounded model checking tool CBMC to beused specifically like one would C code in regular unit tests. The project currently only supportssymbolically reasoning about primitive types and strings which is why this thesis explores thedesign of a domain specific language extension for the rUnit project that explores how the projectcould extend to abstract data types by first extending it with singly linked lists. The project alsouses taxonomy to differentiate between the types of constraints an end-user might want to set onthe lists and discusses how useful taxonomy was to the implementation of the extension. Differentencoding strategies for implementing the extension and evaluated including a novel strategy thatmakes use of CBMC pre-processing to array allocate the memory necessary lists. To evaluateagainst unit tests designed to be similar to property-based tests are used.