k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

RE: [[K-user] ] Learning model checking and K

From: "Chen, Xiaohong" <xc3 AT illinois.edu>
To: Daniel Schnetzer Fava <danielsf AT ifi.uio.no>, "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
Subject: RE: [[K-user] ] Learning model checking and K
Date: Wed, 1 Mar 2017 14:59:36 +0000
Accept-language: en-US

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

[[K-user] ] Learning model checking and K, Daniel Schnetzer Fava, 03/01/2017
- Re: [[K-user] ] Learning model checking and K, Dorel Lucanu, 03/01/2017
  - Re: [[K-user] ] Learning model checking and K, Daniel Schnetzer Fava, 03/01/2017
- RE: [[K-user] ] Learning model checking and K, Chen, Xiaohong, 03/01/2017
  - Re: [[K-user] ] Learning model checking and K, Daniel Schnetzer Fava, 03/01/2017