k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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

From: Dorel Lucanu <dorel.lucanu AT gmail.com>
To: Daniel Schnetzer Fava <danielsf AT ifi.uio.no>
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 14:29:16 +0200

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