K-user mailing list

[<daparpon AT dsic.upv.es>]

Hi! I attempted to follow your advice and apply the debugger to check that the
structures used in the verification rules correspond to actual execution
states. However, whenever I launch the debugger, I get a "[ERROR] Failed to
construct terminal; falling back to unsupported" message, although an initial
configuration is effectively built and the debugger command line activates. I
first ignored it and try to step forward, but then I get another error:

"[Error] Critical: Compute Graph with Pattern Matching Not Implemented Yet"

And, this time, the debugger execution aborts. Could it be an issue related to
the version of K? Is the prover built on further versions, with the debugger
consequently updated?

I am also interested in the idea of launching the prover in IntelliJ's
debugger, but I have not found any instructions on how to prepare the IntelliJ
Idea environment to run/debug modules of K (version with prover) such as
kompile or krun. Do you know where I can find them, or could you please give
me some notes on setting up the environment?

Thanks for your help and sorry for the inconveniencies,
Daniel

----------------------------------------------------------------------------------------------------
On Tue, Nov 07, 2017 at 06:07:38PM +0000, 
hildenb2 AT illinois.edu
 wrote:

Hey Daniel,

Sorry for the very late reply.

There isn't a whole lot of documentation on using the K prover, though we are
actively trying to make interacting with the existing prover easier/smoother.

Unfortunately, when the prover cannot prove something, it usually does just
throw assertion errors and the like. One technique we use is running the
prover
in IntelliJ's debugger to see what queries it's making to Z3 as it's
attempting
to prove your overall goal.

Also, it's often the case that the thing you're trying to prove actually
doesn't
quite make sense. Running the K debugger can help to illuminate these issues.

```sh
$ krun --debugger file-to-run-in-debugger.c
```

You can use the step command (with `s`) to take one execution step, the peek
command (with `p`) to inspect the current state, and the back command (with
`b`)
to move back a step. The run command (with `r`) will run the definition to
completion. Often you can catch bugs in your program just by stepping through
the debugger.

You may consider joining our public Slack/Riot channel to get more immediate
feedback/help from us on your goals. @pdaian can you post details in this
thread
on how to do that?

Let us know what further questions you have,
Everett H.

----------------------------------------------------------------------------------------------------
On Thu, Nov 02, 2017 at 08:39:04AM -0500, 
daparpon AT dsic.upv.es
 wrote:

Hi! I am deeply interested in the procedures followed by the verification
infrastructure of K, in order to create K specifications (and prove them) for
potentially any program in languages for which K semantics have been defined.
As such, I downloaded the infrastructure provided by the K Team in the URL:

https://github.com/kframework/k/wiki/Program-Verification

and tried to produce a specification file for a program in KernelC, based on
the examples available in the distribution. My program works as expected
according to the semantics of KernelC, when executed by the standard mode of
Krun. However, I cannot create verification rules from scratch which would
actually work, with many of them throwing AssertionErrors or delivering a "No
results" as output. I am trying to stick to programs that are similar to the
examples, for starters, and consequently defining similar specifications, but
they do not seem to work out.

I installed and tested the verification infrastructure as specified in the URL
above from the Wiki, and the examples work fine. Then, my issue is most likely
a problem of lack of knowledge on the tool, and how the verification machinery
operates. Is there any manual available on program verification, which covers
further than just installation and testing? Or, at least, could you please
give me some notes on it? I would highly appreciate that.

Thanks in advance and sorry for the inconveniencies.
Best regards,
Daniel