K tool

𝕂 framework distilled. 𝕂 is a rewrite-based executable semantic framework in which programming languages, type systems, and formal analysis tools can be defined using configurations, computations and rules. Configurations organize the state in units called cells, which are labeled and can be nested. Computations are special nested list structures sequentializing computational tasks, such as fragments of program. 𝕂 (rewrite) rules make it explicit which parts of the term they read-only, write-only, read-write, or do not care about. This makes 𝕂 suitable for defining truly concurrent languages even in the presence of sharing. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted. This makes 𝕂 suitable for defining control-intensive features such as abrupt termination, exceptions or call/cc. This paper presents an overview of 𝕂 Framework and the 𝕂 Tool, focusing on the interaction between the 𝕂 Tool and Maude.

References in zbMATH (referenced in 18 articles , 2 standard articles )

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

  1. Haustermann, Michael; Mosteller, David; Moldt, Daniel: Model checking of synchronized domain-specific multi-formalism models using high-level Petri nets (2021)
  2. Ştefănescu, Andrei; Ciobâcă, Stefan; Mereuta, Radu; Moore, Brandon; Roşu, Grigore; Şerbănuṭă, Traian Florin: All-path reachability logic (2019)
  3. Biernacka, Małgorzata; Charatonik, Witold; Zielińska, Klara: Generalized refocusing: from hybrid strategies to abstract machines (2017)
  4. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  5. Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2017)
  6. Rusu, Vlad; Lucanu, Dorel; Şerbănuţă, Traian-Florin; Arusoaie, Andrei; Ştefănescu, Andrei; Roşu, Grigore: Language definitions as rewrite theories (2016)
  7. Arusoaie, Andrei; Lucanu, Dorel; Rusu, Vlad: Symbolic execution based on language transformation (2015)
  8. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei; Nowak, David: Verifying reachability-logic properties on rewriting-logic specifications (2015)
  9. Roşu, Grigore: From rewriting logic, to programming language semantics, to program verification (2015)
  10. Asăvoae, Irina Măriuca; de Boer, Frank; Bonsangue, Marcello M.; Lucanu, Dorel; Rot, Jurriaan: Bounded model checking of recursive programs with pointers in K (2013)
  11. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
  12. Lazar, David; Arusoaie, Andrei; Şerbǎnuţǎ, Traian Florin; Ellison, Chucky; Mereuta, Radu; Lucanu, Dorel; Roşu, Grigore: Executing formal semantics with the (\mathbbK) tool (2012) ioport
  13. Lucanu, Dorel; Şerbănuţă, Traian Florin; Roşu, Grigore: (\mathbbK) framework distilled (2012) ioport
  14. Meseguer, José: Twenty years of rewriting logic (2012)
  15. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2011)
  16. Roşu, Grigore; Ellison, Chucky; Schulte, Wolfram: Matching logic: an alternative to Hoare/Floyd logic (2011)
  17. Simmons, Robert J.; Pfenning, Frank: Logical approximation for program analysis (2011)
  18. Chira, Camelia; Şerbănuţă, Traian Florin; Ştefănescu, Gheorghe: P systems with control nuclei: the concept (2010)