k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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

From: Daniel Schnetzer Fava <danielsf AT ifi.uio.no>
To: Dorel Lucanu <dorel.lucanu AT gmail.com>
Cc: "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 12:31:44 +0000
Accept-language: en-US, nb-NO

I cloned the git repo. Right now I am on commit 35df078e85e83f23d1b45e7eee5481a8cb9e8939, on the master branch.

Daniel

On 1 Mar 2017, at 13:29, Dorel Lucanu <dorel.lucanu AT gmail.com> wrote:

What version of K do you use?
Dorel

On Wed, Mar 1, 2017 at 11:11 AM, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

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