Formal Methods in Software Engineering

K Workshop 2011

March 9, 2018

2nd International Workshop on K Framework K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined making use of configurations, computations and rules.
  • Configurations organize the system/program state in units called cells, which are labeled and can be nested.
  • Computations carry "computational meaning" as special nested list structures sequentializing computational tasks, such as fragments of program; in particular, computations extend the original language or calculus syntax.
  • K (rewrite) rules generalize conventional rewrite rules by making it explicit which parts of the term they read-only, write-only, or do not care about. This distinction makes K a suitable framework for defining truly concurrent languages or calculi even in the presence of sharing.
Since computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted, K is particularly suitable for defining control-intensive language features such as abrupt termination, exceptions or call/cc. (read more) Date and Location: 8-12 August, Cheile Gradistei, Romania The initial page of the event was on the K Framework domain: http://www.kframework.org/K11/

Steering Committee

  • Chucky Ellison (University of Illinois at Urbana-Champaign, USA)
  • Dorel Lucanu (Alexandru Ioan Cuza University of Iasi, Romania)
  • Grigore Rosu (University of Illinois at Urbana-Champaign, USA)

Program Committee

Organizing Committee

  • Andrei Arusoaie, UAIC
  • Radu Mereuta, UAIC
  • Irina Mariuca Asavoae, UAIC
  • Mihai Asavoae, UAIC
  • Lucian Gadioi, UAIC
  • Gheorghe Grigoras, UAIC

Preproceedings:

k-2011-preproceedings-final-original k-2011-preproceedings-final-corrected