k-user AT lists.siebelschool.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] Twelf

From: "Rosu, Grigore" <grosu AT illinois.edu>
To: Suminda Dharmasena <sirinath AT sakrio.com>, "info AT kframework.org" <info AT kframework.org>, "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: Re: [K-user] Twelf
Date: Wed, 1 Jan 2014 16:26:02 +0000
Accept-language: en-US
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

I cannot agree more. In fact, the language definition IS the language, so nothing else should be needed for program verification. Our matching logic formalism for static property specification and the reachability logic formalism for dynamic property specification are designed precisely in this spirit: just use the formal language definition for everything.

Grigore

From: Suminda Dharmasena [sirinath AT sakrio.com]
Sent: Wednesday, January 01, 2014 12:25 AM
To: info AT kframework.org; k-user AT cs.uiuc.edu
Subject: Re: Twelf

All formal specification and verification ideally should be built in to the language definition.

On 1 Jan 2014 11:18, "Suminda Dharmasena" <sirinath AT sakrio.com> wrote:

http://twelf.org

I am new to both. Played with Twelf for less than a hour. Perhaps you can borrow some ideas from Twelf.

Re: [K-user] Twelf, Suminda Dharmasena, 01/01/2014
- Re: [K-user] Twelf, Rosu, Grigore, 01/01/2014
  - Re: [K-user] Twelf, Suminda Dharmasena, 01/02/2014