Right now, many classes have ad-hoc tests in their main-methods. Create new plugin and appropriate test cases.

The verification-systems are currently included statically in to the project. This shall be dynamized by allowing a definition of all relevant classes/options in an "ini" file, so the solver can be loaded more independently.

I started to evaluate hypotheses with Java only (de.tubs.isf.gudio.core.statistics.tests) but haven't finished it so far

The core hypotheses and cost network have to be addopted to support at least quadratic optimization.
This means the not only two options shall be compared with each other, rather sets of options. This means the tools and the guido.core need to be support multiple options and their interactional terms.

de.tu.bs.isf.guido.verification.systems should be de.tubs.isf.guido.verification.systems.
And: the packages are missing the isf part...

Is it possible to use the date to explore new hypotheses for upcoming tests?

Implement a new package with the name de.tubs.isf.gudio.core.statistics.explore. Implement techniques to "guess" good hypotheses. Evaluate the results with 10x cross validation.

This package should provide numerous programs to gather and visualize evaluation statistics.

• Which contuniation mechanism performs best?
• Comparsion with default and random
• ...?

Please extend this list.

The very important characteristic

METHOD_CALLS_SPEC_TRUE (i.e., whether called methods have a contract)

is not resolved due to problems (runtime errors/method not found stuff) with javaparser. Either we need to fix these problems or we have to come up with a resolution on our own...

How does KeY handle this stuff?

We should an UI for the server/client structure

For instance, the following statistics might be interesting:

• Get the best configuration for a specific contract, language construct etc.
• Get the worst configuration for a specific contract, langauge construct, etc.
• Get the ratio of to what extent a specific option was succesfull (i.e., when optionA was selected, successrate was 100%)
• Get the best overall configuration for provability (the one that closed the most)
• Combine the best overall configuration with the successrate of an option
• Give a sorted list of configuration with infos such as how many proofs were closed with this one and how often was the configuration applied. Maybe also which contracts were closed and which were not.
• Give a sorted list of subjects (proofs) with infos, such as which configurations were the fastest...

Create test resources and tests as can be seen in numerous main methods

Create main guido program in de.tubs.isf.guido.prover.

Things to consider:

• How to apply a contuniation mechanism
• How to solve the CSP elegenatly
• How to configure guido? (Timeout/continuitation mechanism)
• what about the rule-based system?

Input should be a source file and the evelatuated hypotheses

The whole project needs to be refactored, so it becomes more flexible and independent from KeY.

I think it is better to move the generic stuff from the verification system plugin to the core plugin (i.e., the whole job thing):

The new package could be de.tubs.guido.core.system. Moreover, this generic stuff needs some rework.

• BatchXMLHelper is too KeY specific. There also exists the same file with the name KeyBatchXMLHelper, which extends the batchXMLHelper. Maybe it is better to create an IBatchXMLHelper with the getJobs-methods and let be implemented individually by each system (as done by KeyBatchXMLHelper)
• The same goes for the Job-class, which is too KeY specific. Create the interface IJob, such that KeyJob implements IJob

Move the respective generic structures to the core package:

Each system then needs to implement the structures as done for KeY in the verification-system plugin.