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. Occasionally, code duplication can be helpful to decouple systems; however, undesired clones complicate 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 Moss or JCCD. While batch-processing a set of Isabelle theory files is an important use-case, the clone detection tool should also run in an interactive session to give hints about potential duplications.

Programming language:
Scala

Prerequisites:
Familiarity with Scala; English

Supervisor:
Fabian Huch, email {huch} AT [in.tum.de]

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