K-user mailing list

[<daparpon AT dsic.upv.es>]

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