K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Dorel and other K users,

Sorry for the spam, but to minimize spam, please send such messages directly to me.  I will then update the respective problems/challenges and check it with you.  It would be ideal if you send me the DOI of the papers that you want me to cite.

Thank you,

Grigore

 

 

---

From: Dorel Lucanu [dlucanu AT info.uaic.ro]
Sent: Monday, February 29, 2016 12:46 PM
To: k-user AT lists.cs.illinois.edu
Subject: Re: [[K-user] ] K-related open problems and challenges

Dear Grigore,

Here are several papers that are strong related to the open problems and challenges from your list:

Semantics of K &&
=========
Systematic comparison of K with other operational approaches
======================================

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian-Florin Serbanuta, Andrei Stefanescu, Grigore Rosu: Language Definitions as Rewrite Theories. WRLA 2014: 97-112

together with its journal version:

Vlad Rusu, Dorel Lucanu, Traian-Florin Serbanuta, Andrei Arusoaie, Andrei Stefanescu, Grigore Rosu: Language definitions as rewrite theories. J. Log. Algebr. Meth. Program. 85(1): 98-120 (2016)
http://www.sciencedirect.com/science/article/pii/S2352220815000838

" In this paper we investigate the theoretical relationship between Klanguage definitions and their Maude translations, between symbolic extensions of Kdefinitions and their Maude translations, and how the relationship between K definitions and their symbolic extensions is reflected on their respective representations in Maude. In particular, the results show how analysis performed with Maude tools can be formally lifted up to the original language definitions."

Symbolic execution framework
==================

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu: A Generic Framework for Symbolic Execution. SLE 2013: 281-301

together with its journal version:

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu: Symbolic execution based on language transformation. Computer Languages, Systems & Structures 44: 48-71 (2015)
http://www.sciencedirect.com/science/article/pii/S147784241500055X

"We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language definition is generated, with the same syntax as the original one, but whose semantical rules are transformed in order to rewrite over logical formulas denoting possibly infinite sets of program states. Then, the symbolic execution of concrete programs is, by definition, the execution of the same programs with the symbolic semantics. We prove that the symbolic execution thus defined has the properties naturally expected from it (with respect to concrete program execution)."


Coinductive program verification  &&
====================      
Formal Relationship between the Circularity proof rule and Coinduction &&
============================================
Symbolic execution framework
==================

Dorel Lucanu, Vlad Rusu, Andrei Arusoaie. A Generic Framework for Symbolic Execution: Theory and Applications
Journal of Symbolic Computation, Elsevier, 2016, to appear

A preliminary technical report can be found at

https://hal.inria.fr/hal-01238696v2

"We  show how a coinduction-based extension of symbolic execution can be used for the deductive verification of programs. We show how the proposed symbolic-execution approach, and the coinductive verification technique based on it, can be seamlessly implemented in language definition frameworks based on rewriting such as the K framework. "

Language-independent infrastructure for program equivalence &&
======================================  
Formal Relationship between the Circularity proof rule and Coinduction
============================================

Dorel Lucanu, Vlad Rusu: Program Equivalence by Circular Reasoning. IFM 2013: 362-377

together with its journal version:

Dorel Lucanu, Vlad Rusu: Program equivalence by circular reasoning. Formal Asp. Comput. 27(4): 701-726 (2015)

" We propose a logic and a deductive system for stating and automatically proving the equivalence of programs written in languages having a rewriting-based operational semantics. The chosen equivalence is parametric in a so-called observation relation, and it says that two programs satisfying the observation relation will inevitably be, in the future, in the observation relation again. This notion of equivalence generalises several well-known equivalences and is appropriate for deterministic (or, at least, for confluent) programs. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the given program-equivalence problem. We show that our approach is suitable for proving equivalence for terminating and non-terminating programs as well as for concrete and symbolic programs."

K semantics to new real languages
=====================

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu: Towards a K Semantics for OCL. Electr. Notes Theor. Comput. Sci. 304: 81-96 (2014)
http://www.sciencedirect.com/science/article/pii/S1571066114000401

" We give a formal definition to a significant subset of the Object Constraint Language (OCL) in the K framework. The chosen subset includes the usual arithmetical, Boolean (including quantifiers), and string expressions; collection expressions (including iterators and navigation); and pre/post conditions for methods. Being executable, our definition provides us, for free, with an interpreter for the chosen subset of OCLl. It can be used for free in K definitions of languages having OCL as a component."

Vlad Rusu, Dorel Lucanu: A K-Based Formal Framework for Domain-Specific Modelling Languages. FoVeOOS 2011: 214-231
http://link.springer.com/chapter/10.1007%2F978-3-642-31762-0_14

"We propose a formal approach for the definition of domain-specific modelling languages (DSMLs). The approach uses basic Model-Driven Engineering artifacts for defining a DSML’s syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by mapping them to the 𝕂K semantic framework. "


If you need more details on the papers or if you want to include  (a part of ) them in the list and you need my help for that, please let me know.

Best regards,
Dorel

On 27/02/16 15:36, Rosu, Grigore wrote:

Dear K users,

We have recently compiled a list of open problems and challenges related to K and its foundations at:

    http://fsl.cs.illinois.edu/index.php/Open_Problems_and_Challenges

Please feel free to contact us if you are interested in any of these problems, or if you are already working on any of them.

Best,
Grigore