[isabelle] Clone detection for Isabelle theories



Dear list,

I'd like to announce the availability of a technology preview of code
clone detection for Isabelle theories.

This is the result of a Master's Thesis carried out by Dominik Vinan
under my supervision, with the help of Benjamin Hummel. Benjamin's
company is the vendor of ConQAT, an open-source software quality
assurance toolkit, for which the student has implemented an Isabelle
frontend.

The purpose of code clone detection is simple: to find duplicated
specification or proof fragments in Isabelle theories.

I will present the tool and its accompanying paper at the Isabelle
Workshop in Nancy, but it is already possible to download and use it:

  Paper
  <http://www.in.tum.de/~nipkow/Isabelle2016/Isabelle2016_9.pdf>

  ConQAT+Isabelle bundle

<https://www21.in.tum.de/~hupel/downloads/isabelle-clones/isabelle-clones-preview.zip>

The bundle should contain all instructions for feeding theories into
ConQAT. It should work on macOS and Linux (no guarantees for Windows).
The result is an HTML report of detected clones which can be viewed in
the browser.

If you try it out, please report any problems (or that you didn't have
problems) to me via mail so that the student and me can iron out bugs
before ITP.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.