k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] Model_Checking in K

From: samira kherfellah <samira.kherfellah AT gmail.com>
To: k-user AT cs.uiuc.edu
Subject: [K-user] Model_Checking in K
Date: Wed, 1 May 2013 13:48:40 +0200
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

Hi All,

In k, to represent the model_checking, LTL formulas are used. (two modules, one for the syntax and an another for the semantics ).

But how to evaluate performance of model_checking in K?

For example, how can we have the execution time, the occupation of the memory?

Sincerely,
Samira

[K-user] Model_Checking in K, samira kherfellah, 05/01/2013
- Re: [K-user] Model_Checking in K, Dorel Lucanu, 05/01/2013