K Prover

K Prover. An overview of the K semantic 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 explicit which parts of the term they read, write, 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. This paper gives an overview of the K framework: what it is, how it can be used, and where it has been used so far. It also proposes and discusses the K definition of Challenge, a programming language that aims to challenge and expose the limitations of existing semantic frameworks.


References in zbMATH (referenced in 41 articles , 1 standard article )

Showing results 1 to 20 of 41.
Sorted by year (citations)

1 2 3 next

  1. Fava, Daniel S.; Steffen, Martin; Stolz, Volker: Operational semantics of a weak memory model with channel synchronization (2019)
  2. Johansen, Christian; Owe, Olaf: Dynamic structural operational semantics (2019)
  3. Ştefănescu, Andrei; Ciobâcă, Stefan; Mereuta, Radu; Moore, Brandon; Roşu, Grigore; Şerbănuṭă, Traian Florin: All-path reachability logic (2019)
  4. van Binsbergen, L. Thomas; Mosses, Peter D.; Sculthorpe, Neil: Executable component-based semantics (2019)
  5. Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
  6. Arusoaie, Andrei; Ciobâcă, Ştefan; Lucanu, Dorel; Rosu, Grigore; Rusu, Vlad; Şerbănuţă, Traian-Florin: Program logics and their applications (2017)
  7. Biernacka, Małgorzata; Charatonik, Witold; Zielińska, Klara: Generalized refocusing: from hybrid strategies to abstract machines (2017)
  8. Bugliesi, Michele; Calzavara, Stefano; Focardi, Riccardo: Formal methods for web security (2017)
  9. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  10. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
  11. Roşu, Grigore: Matching logic (2017)
  12. Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
  13. Rusu, Vlad; Lucanu, Dorel; Şerbănuţă, Traian-Florin; Arusoaie, Andrei; Ştefănescu, Andrei; Roşu, Grigore: Language definitions as rewrite theories (2016)
  14. Şerbănuţă, Traian Florin; Dinu, Liviu P.: Maximally parallel contextual string rewriting (2016)
  15. Arusoaie, Andrei; Lucanu, Dorel; Rusu, Vlad: Symbolic execution based on language transformation (2015)
  16. Bogdanas, Denis; Roşu, Grigore: K-Java: a complete semantics of Java (2015)
  17. Ciobâcă, Ştefan; Lucanu, Dorel; Rusu, Vlad; Roşu, Grigore: A theoretical foundation for programming languages aggregation (2015)
  18. Lucanu, Dorel; Rusu, Vlad: Program equivalence by circular reasoning (2015)
  19. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei; Nowak, David: Verifying reachability-logic properties on rewriting-logic specifications (2015)
  20. Mota, A.; Farias, A.; Woodcock, J.; Larsen, P. G.: Model checking CML: tool development and industrial applications (2015) ioport

1 2 3 next


Further publications can be found at: http://www.kframework.org/index.php/K_Publications