Frequently Asked Questions about KeYmaera

Table of Contents KeYmaera FAQ General Questions about KeYmaera Where can I read about the KeYmaera approach Installing and Configuring KeYmaera KeYmaera or KeYmaera Webstart do not work but do not tell me why KeYmaera could not load JLink native library KeYmaera could not find MathLink executable KeYmaera starts but when I prove anything it just hangs or performs strangely Segmentation fault or Java Virtual Machine panic KeYmaera sources do not compile Loading Problems in KeYmaera I want to open an example in KeYmaera KeYmaera reports a syntax error in my input file KeYmaera reports a syntax error with different line numbers Using KeYmaera to Find Proofs KeYmaera is busy proving my problem but I do not see what it does. Can I stop and look? Depending on the backend, KeYmaera sometimes works unexpectedly. KeYmaera proves several properties but it does not prove my current property Interacting with KeYmaera to Solve Complicated Problems KeYmaera stops at some point without having found a proof. Is my system broken? How do I apply a proof rule manually? How can I go back and undo proof rules to try something else? I cannot find a counterexample I cannot see the transition system. I want to visualize what my hybrid program does. KeYmaera is stuck and does not even try to continue I have a different question	Download or Launch KeYmaera

KeYmaera FAQ

KeYmaera is a verification tool for hybrid systems and built as a hybrid theorem prover for hybrid systems. Here we collect answers to frequently asked questions.

General Questions about KeYmaera

Where can I read about the KeYmaera approach

Problem:

I am looking for a reference on KeYmaera and want to understand how KeYmaera works.

Solution:

The most comprehensive description of the KeYmaera approach can be found in the book about the KeYmaera approach. Other canonical references on the KeYmaera approach are an article in J. Autom. Reas. and J. Log. Comput. Together, these references give a good overview of what KeYmaera is doing. Also see the publication reading guide for more recommended readings on other parts of KeYmaera.

Installing and Configuring KeYmaera

KeYmaera or KeYmaera Webstart do not work but do not tell me why

Problem:

The installed KeYmaera or the KeYmaera Webstart do not work, but I cannot see errors or exceptions.

Solution:

Make sure that you have enabled the Java Console to see error outputs produced by KeYmaera / KeYmaera Webstart, that may otherwise go unnoticed. These exceptions can be helpful in finding out what went wrong. Depending on the operating system and browser, the Java Console can be enabled in the Java Plug-in or Java System Preferences or in the browser preferences.

Besides, we encourage you to read through all questions and solutions in this FAQ to see if your issue is described and solved in more detail.

KeYmaera could not load JLink native library

Problem:

KeYmaera complains that it cannot find a native library JLinkNativeLibrary required for interfacing with Mathematica. It outputs an exception like

Fatal error: cannot find the required native library named
JLinkNativeLibrary.
java.lang.UnsatisfiedLinkError:
  com.wolfram.jlink.NativeLink.MLOpenString
      (Ljava/lang/String;[Ljava/lang/String;)J
  at com.wolfram.jlink.NativeLink.MLOpenString(Native Method)
  at com.wolfram.jlink.NativeLink.<init>
  at com.wolfram.jlink.MathLinkFactory.createMathLink0
  at com.wolfram.jlink.MathLinkFactory.createMathLink
  at com.wolfram.jlink.MathLinkFactory.createKernelLink0
  at com.wolfram.jlink.MathLinkFactory.createKernelLink
  at de.uka.ilkd.key.dl.arithmetics.impl.mathematica.
      KernelLinkWrapper.createLink (KernelLinkWrapper.java:256)

Solution:

The path to the JLink native library is wrong or the native library does not match match the computer CPU (Intel, PowerPC, ...) and architecture (x86-32bit or x86-64bit, ...). To change the jlink native library path use Options->Tool Paths menu. In the dialog that opens, look at the tab Mathematica Properties and make sure that the paths are entirely correct. Click apply and double check the MathKernel path and J/Link native directories. Also make sure that the J/Link path matches your system architectyre. Restart KeYmaera after changing this option.

Note that some systems will give you a hard time if you are using a space character or other special characters in any of the folder names. We recommend not to install Mathematica into directories like

C:\Program Files\Wolfram Research\Mathematica\8.0

Instead install it into a folder without spaces like

C:\Wolfram\Mathematica\8.0

KeYmaera could not find MathLink executable

Problem:

KeYmaera throws an exception saying that it could not find MathLink executable like the following

java.rmi.RemoteException: Could not initialise math link;
  nested exception is: 
  MathLinkException: 1004: Could not find MathLink executable.
  at de.uka.ilkd.key.dl.arithmetics.impl.mathematica.
      KernelLinkWrapper.createLink (KernelLinkWrapper.java:308)

Solution:

Please check the path set to the file MathKernel. To change this path, use Options->Tool Paths menu. In the dialog that opens, look at the tab Mathematica Properties and make sure that the paths are entirely correct. Click apply and double check the MathKernel path and J/Link native directories. Make sure you can execute that file to call the kernel of Mathematica. Check if the MathKernel can compute expressions like 3+4.5 successfully.

KeYmaera starts but when I prove anything it just hangs or performs strangely

Problem:

KeYmaera starts and I can click on prove. But when I do, it either hangs at a low percentage (5% for instance) or performs very strangely.

Solution:

Make sure that your Mathematica can run successfully. Make sure you can execute that file to call the kernel of Mathematica. Check if the MathKernel can compute expressions like 3+4.5 successfully and that you do not have any licensing issues. Also double check that you have selected the right paths in Options->Tool Paths menu. In the dialog that opens, look at the tab Mathematica Properties and make sure that the paths are entirely correct. Click apply and double check the MathKernel path and J/Link native directories. If you get the paths wrong, KeYmaera only works partially or may not work at all. Check for the issues and solutions mentioned on Mathematica J/Link. Check that you have configured KeYmaera options appropriately. If you use a slow arithmetic procedure or bad settings, do not be surprised if your proof takes a very long time. Please check KeYmaera's console output for warnings and errors.

Segmentation fault or Java Virtual Machine panic

Problem:

KeYmaera crashes with a segmentation fault or the Java Virtual Machine panics.

Solution:

Most likely, the J/Link native library path that you specified in the KeYmaera settings is incompatible with the Java Virtual Machine and platform that you are using. Make sure you indicate a path to the J/Link native library that actually matches the computer CPU (Intel, PowerPC, ...) and code (x86-32bit or x86-64bit, ...). To change this path see Options->Tool Paths menu, then in the tab Mathematica Properties make sure the paths are okay. Click apply and double check the MathKernel path and J/Link native directories. Restart KeYmaera after changing these options.

KeYmaera sources do not compile

Problem:

Calling make gives an error when compiling the KeYmaera sources.

Solution:

Make sure that you have installed all required base libraries in key-ext-jars/ and triplecheck that you have all the right versions of libraries and software installed. Read the file README.keymaera and carefully follow all instructions. Do not work with different versions of the library files or put them in wrong places unless you know exactly what you are doing.

Loading Problems in KeYmaera

I want to open an example in KeYmaera

Problem:

KeYmaera starts perfectly, but I do not know how to start working on an example problem or case study

Solution:

Use the menu File->Load Project to open one of the example projects from the KeYmaera library. You can also create your own KeYmaera problem using a text editor or the KeYmaera Eclipse plugin and open this problem in KeYmaera using File->Load.

KeYmaera reports a syntax error in my input file

Problem:

KeYmaera reports a syntax error in my input file or throws a parse exception

Solution:

Use the Details provided in the error message to locate the syntax problem. When checking parse errors, be aware that error locations may be relative to the start of the hybrid program, not relative to the start of the key problem specification file. We apologize for this inconvenience, which is caused by the flexible parsing language of KeYmaera. Please check your file carefully against the KeYmaera syntax.

You may have an easier time spotting the problem when you use the KeYmaera Eclipse plug-in.

Also see full description of KeY files and description of logical formulas in KeYmaera.

KeYmaera reports a syntax error with different line numbers

Problem:

KeYmaera reports a syntax error in my input file or throws a parse exception, but it reports multiple lines or but I can't find the line that KeYmaera reports.

Solution:

KeYmaera may report both the actual line number where the error occurs, and the relative line number, i.e., relative to the start of the respective hybrid program modality. What you should do in is look at the line:column that was reported in the beginning of the parse error.

You may also have an easier time spotting the problem when you use the KeYmaera Eclipse plug-in. It understands the grammar of KeYmaera files, supports syntax highlighting, auto completion, error reporting, refactoring and many other features.

Using KeYmaera to Find Proofs

KeYmaera is busy proving my problem but I do not see what it does. Can I stop and look?

Problem:

KeYmaera is busy with searching for a proof of my problem, but it takes time and I want to see what it is doing.

Solution:

Click the stop button in the toolbar or use the Proof->Stop menu. Patiently wait until KeYmaera comes to a well-defined point where you can inspect the proving process. Unfortunately, this may take some time, depending on the proof complexity. Then look at the proof status (the last rule application is shown at current node). If you want to continue with proof search, just click the start toolbar button again or Proof->Start. For more verbose status information about what is going on during proof search, also look at KeYmaera's console output.

Note that if KeYmaera still does not stop, you can often force it stop with a bit of a hack. Launch a second instance of KeYmaera, open an arbitrary problem, hit Proof->Start and then Proof->Stop.

Depending on the backend, KeYmaera sometimes works unexpectedly.

Problem:

When I change from one backend to the other, KeYmaera behaves differently than I expect. With some backends it proves properties that it cannot prove with others.

Solution:

Except for expert users, we recommend following the naming convention to start all variables with lowercase letters. This avoids surprises with built-in meaning for some backends. In addition, the backends have different sweetspots and may be able to prove some properties better but others worse. That is why you can choose the backend in the KeYmaera settings.

KeYmaera proves several properties but it does not prove my current property

Problem:

I firmly believe that the specification for my system holds true, but KeYmaera cannot prove it

Solution:

Check which arithmetic handling back-end and Proof-Settings you are using. Make sure you install and configure at least one of the following options:

• Mathematica (optional, recommended)
• Reduce/Redlog (optional)
• QEPCAD B or QEPCAD B for Mac (optional)
• HOL Light (optional)
• Cohen-Hörmander Quantifier Elimination (optional)
• CSDP (optional)

In the Hybrid Strategy tab, choose your proving back-end for the real arithmetic solver, equation solver, differential equations, counterexample tool, and arithmetic simplifier options. There are numerous other options with which you can control the proving power of KeYmaera. Make sure configure KeYmaera options for arithmetic properly.

If KeYmaera still is not able to prove your example, the problem conjecture may be wrong due to a counterexample. If you are certain that your conjecture is right, you can help KeYmaera to prove the problem using user interactions or proof annotations. For instance, you could provide invariants, hide complicated formulas from the arithmetic handling etc.

Interacting with KeYmaera to Solve Complicated Problems

KeYmaera stops at some point without having found a proof. Is my system broken?

Problem:

KeYmaera reads my problem file, I hit Proof->Start, and the KeYmaera prover starts working on it. After a while KeYmaera stops but does not report a proof. Is my system broken?

Solution:

If KeYmaera does not find a proof, or only finds a proof for a part of the property, that does not mean that your system is broken. It only means your system is broken if you also find an appropriate counterexample using the various counterexample rules that shows that there is a problem. Otherwise, it may just mean that KeYmaera's automation techniques have not found a proof for your system. Often times, this means that you have not specified the right parameter constraints. Or that you have not yet found out good controllability constraints for your system. Or that you have simply specified your system in a way that KeYmaera's automation techniques cannot yet handle well enough. Perhaps, your system has also not been designed very well yet.

Don't despair. This just means that you need to think harder and understand your problem better. Identify useful variable constraints and explain them to KeYmaera. Did you encode important state information in bits and modes? Don't do that without explaining to KeYmaera what the pieces mean, e.g., using appropriate invariants. Remove some repetition * or unwind loops to look at bounded transition problems first. Try a proof using a formula that looks like the right invariant to you. Look at the formulas in the open goals and take the formulas and counterexamples serious. Did you forget to specify something? Is there a criticial relationship among the variables that you should specify? Work interactively with KeYmaera to explore your system.

How do I apply a proof rule manually?

Problem:

KeYmaera's proof strategy is useful but I want to apply a proof rule manually

Solution:

KeYmaera has a number of powerful proof strategies and can be tuned to perform even better by configuring KeYmaera options. Nevertheless, for learning purposes, for experimenting with and exploring different system designs, and for helping KeYmaera to find proofs, it can be really useful to apply proof rules manually. But how do I apply proof rules manually?
In the Current Goal view, choose a formula that you want to apply a proof rule to. Right click on the formula to open the context popup menu, which will list all applicable proof rules. Select which proof rule you want to use. When you hold the mouse over a proof rule, it will give you a preview of what will happen if you apply it. But you can also just select a proof rule, see what happens if you use it, and if you are not happy with the result use Proof->Goal Back to undo the proof rule.

How can I go back and undo proof rules to try something else?

Problem:

KeYmaera's proof strategy or I have applied some proof rules that do no longer look promising to me. How can I go back and try something else?

Solution:

KeYmaera has a number of powerful proof strategies but as a user with domain knowledge about the problem I know that the one thing that KeYmaera tried on one of the proof branches does not look promising. How can I go back and let KeYmaera try something else? Perhaps, I have even tried a number of proof rules but they no longer look promising to me now. I want to go back.

In order to go back, stop KeYmaera using Proof->Stop if it is still running (if KeYmaera has stopped already, skip this step). Then choose Proof->Goal Back to undo the last proof rule. You can use Proof->Goal Back repeatedly to undo a couple of steps on the current branch. If you want to undo several proof steps at once, it may be more convenient to locate the last step that you liked in the Proof Tree pane, right click on this proof node to open the popup context menu and choose Prune Proof. This will cut off all proof node descendants at once and you can try something else. Prune Proof is equivalent to a series of Proof->Goal Back steps but may be more convenient. Switch to a different branch if you want to undo proof rules there, too.

I cannot find a counterexample

Problem:

I cannot find the Find Counterexample button or KeYmaera does not find a counterexample for me

Solution:

The search for counterexamples and the Find Counterexample button in the context menu will be hidden unless you have installed and configured a counterexample tool. Please install Mathematica first. In order to find counterexamples, you need to choose go to the Hybrid Strategy tab and choose a counterexample tool from the options. Then the Find Counterexample will be available as a proof rule (when applicable), e.g., to the whole goal in Current Goal view. See applying proof rules.
Using Find Counterexample on a buggy specification for ETCS-simple, for instance, will produce Note that the counterexample value Power[2,Rational[1,2]] found for variable m is the square root √2. Also note that after you found a counterexample, you need to click Proof->Stop to stop searching for counterexamples.

I cannot see the transition system. I want to visualize what my hybrid program does.

Problem:

I cannot generate transition system views for my hybrid programs or I cannot even find the button that would show me a visualization

Solution:

Make sure you have installed a graph visualization tool like graphviz/dotty on your computer. In the Current Goal view just right-click on a hybrid program within the formula to open the context menu for applicable proof rules. Then choose Visualization Rule to generate the transition system view for this hybrid program. This will generate a transition system view in the file placed in /tmp/dottyfile.dot (make sure the path /tmp or \tmp exists on your disk). Any graph visualization tool can be used to display the transition system view placed in /tmp/dottyfile.dot file. If the dotty tool is properly configured and in your system path, then KeYmaera will display the transition system automatically when you use the Visualization Rule. See applying proof rules.
Using the Visualization Rule on ETCS-simple, for instance, will produce For a more realistic model of ETCS, the Visualization Rule shows the following transition system view: Also see the example in Controlled Moving Point and simple aircraft roundabout and water tank.

KeYmaera is stuck and does not even try to continue

Problem:

I have been working with KeYmaera for a while, but all of a sudden it doesn't do anything when I click Proof->Start.

Solution:

When you start and stop proofs a lot, then you can sometimes get KeYmaera confused about its strategy caches, so that KeYmaera thinks it has tried everything already when it really didn't. That is an annoying bug, but fortunately not soundness critical and there's a simple workaround. Just use goal back on the current node, which will make KeYmaera reconsider its options. If the problem persists, you can also just go to Hybrid Strategy, then Advanced Options, and turn on the Reset Strategy option. This will force KeYmaera to clear its caches. Then use Proof->Start.

I have a different question

Problem:

I have a different question about KeYmaera that is not answered here.

Solution:

Please direct your question to the KeYmaera mailing list.