Clone Detection in Isabelle Theories

Chair for Logic and Verification

Bachelor Thesis

Duplicate code segments, or “clones,” typically arise when developers simply copy & paste existing code to form the basis of new code. This practice complicates maintenance, because each bug fix in one such segment must normally be replicated in the other similar segments. In large code bases, clones are difficult to identify because each of the clones has potentially been modified independently of the others. The issue is not restricted to programming languages; the large set of Isabelle theories, included with Isabelle or in the Archive of Formal Proofs, contains many (known and unknown) clones.

The goal of this project is to develop a tool to detect clones in Isabelle theories. The tool should be developed as a frontend to an existing clone detection framework, such as ConQAT (developed at Chair 4) and JCCD. It would parse a large set of Isabelle theory files and make enough information available to the clone detection framework so that it can do its work.

Programming language:
Java

Prerequisites:
Familiarity with Java; English

Supervisor:
Simon Wimmer

Professor:
Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]