k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] To reach a point of a program

From: Alex <alexdba AT gmail.com>
To: "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
Subject: [[K-user] ] To reach a point of a program
Date: Fri, 19 May 2017 18:10:54 +0000

Hi,

We have been using the K-framework to implement the operational semantics
of a process algebra named Circus, which is a combination of CSP and Z.
The current status of our work is fully reported in
https://hal.archives-ouvertes.fr/hal-01438386
We have now a symbolic trace generator for of a good subset of it,
thanks to K!

By now, we are interested in guiding the trace generator.
That means that we want to direct it in order to be sure that a given
point of the program is reached.

Does anyone has some experience in using K for similar purpose?

Thanks for the help!

[[K-user] ] To reach a point of a program, Alex, 05/19/2017
- Re: [[K-user] ] To reach a point of a program, Everett Hildenbrandt, 05/31/2017