K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

Thanks for the information Xiaohong.

I also found more details on this github issue here:

https://github.com/kframework/k/issues/1285

Do you have some intuition on when the support would become available?  I’ll understand if it is too difficult to say… I am sure adding model checking support is far from trivial.

If there is a github issue that is tracking this effort, do you mind sharing the link?

Thanks again,

Daniel Fava

On 1 Mar 2017, at 15:59, Chen, Xiaohong <xc3 AT illinois.edu> wrote:

Dear Daniel,

Thank you for choosing K.

The current K does not support model checking. However, we have been working on
it for a time, and K will support model checking in the future.

As far as I know, K 3.4 does support model checking. You might want to checkout that
version and take a look.

Thank you,
Xiaohong

-------------------------
Chen, Xiaohong
BSc, Peking University
PhD student, UIUC

________________________________________
From: Daniel Schnetzer Fava [danielsf AT ifi.uio.no]
Sent: Wednesday, March 01, 2017 3:11 AM
To: k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] Learning model checking and K

Hi,

I wrote a language definition on K and a small program in that language.

I would now like to check whether a given configuration could have been produced by running that small program, given the language definition.

Can you point me in the right direction?  I would be happy to read documentation on K and model checking.

Thank you!

Daniel Fava