Bachelor thesis
Automated proof-search methods are ubiquitous in Isabelle proofs. As technology progresses, they become faster and more powerful: For example, decision procedures for decidable fragments can suddenly solve problems easily that were previously too hard for automation.
However, performance degradation is also possible: In a large system such as Isabelle, changes in some part of the system can occasionally cause friction in other places ( e.g., such as discussed in this thread). The resulting slow-down may not be noticed immediately as it can affect only certain methods, theories, or even sessions.
By analyzing the underlying performance data, we want to spot such trends immediately. The goal of this thesis is to collect the Isabelle performance data into a storage back-end, extract the trends from the data, and visualize them.
Programming language:
Scala
Prerequisites:
Scala experience; Basic Isabelle knowledge; English
Advisor:
Fabian Huch, email {huch} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]