An overview of the K semantic framework
From MaRDI portal
Publication:987974
DOI10.1016/J.JLAP.2010.03.012zbMATH Open1214.68188OpenAlexW2048417351MaRDI QIDQ987974FDOQ987974
Authors: Grigore Roşu, Traian Şerbănuţă 
Publication date: 24 August 2010
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlap.2010.03.012
Recommendations
- A truly concurrent semantics for the \(\mathbb{K}\) framework based on graph transformations
- Defining and Executing P Systems with Structured Data in K
- K-Maude: a rewriting based tool for semantics of programming languages
- A rewrite framework for language definitions and for generation of efficient interpreters
- Towards a \(\mathbb{K}\)ool future
Theory of programming languages (68N15) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)
Cites Work
- Computer Aided Verification
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Computing with membranes
- Title not available (Why is that?)
- Modular structural operational semantics
- A structural approach to operational semantics
- The power of communication: P systems with symport/antiport
- The chemical abstract machine
- MGS: a rule-based programming language for complex objects and collections
- Conditional rewriting logic as a unified model of concurrency
- A syntactic approach to type soundness
- Title not available (Why is that?)
- A rewriting logic approach to operational semantics
- A rewrite framework for language definitions and for generation of efficient interpreters
- A Rewriting Logic Approach to Type Inference
- Automated Reasoning
- Rewriting logic as a semantic framework for concurrency: a progress report
- The rewriting logic semantics project
- The gamma model and its discipline of programming
- Membrane systems with promoters/inhibitors
- Pragmatics of modular SOS
- Defining and Executing P Systems with Structured Data in K
- Title not available (Why is that?)
- Formal methods for open object-based distributed systems. 9th IFIP WG 6.1 international conference FMOODS 2007, Paphos, Cyprus, June 6--8, 2007. Proceedings.
Cited In (45)
- The rewriting logic semantics project: a progress report
- The rewriting logic semantics project: a progress report
- A framework for modeling the semantics of synchronous and asynchronous procedures with abstract state machines
- Title not available (Why is that?)
- Twenty years of rewriting logic
- Dynamic structural operational semantics
- Executable component-based semantics
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Operational semantics of a weak memory model with channel synchronization
- Maximally Parallel Contextual String Rewriting
- Formally verified animation for RoboChart using interaction trees
- Model checking of synchronized domain-specific multi-formalism models using high-level Petri nets
- Pattern eliminating transformations
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
- \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
- P systems with control nuclei: the concept
- Operational semantics of a weak memory model with channel synchronization
- Symbolic execution based on language transformation
- Matching logic: an alternative to Hoare/Floyd logic
- A truly concurrent semantics for the \(\mathbb{K}\) framework based on graph transformations
- A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
- Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K
- Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
- Implementing type systems for the IDE with Xsemantics
- On the effectiveness of higher-order logic programming in language-oriented programming
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- A lazy desugaring system for evaluating programs with sugars
- K Prover
- Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework
- αCheck: A mechanized metatheory model checker
- Defining and Executing P Systems with Structured Data in K
- Collecting Semantics under Predicate Abstraction in the K Framework
- A Calculus for Language Transformations
- Program equivalence by circular reasoning
- A generic framework for symbolic execution: a coinductive approach
- All-Path Reachability Logic
- Formally understanding Rust's ownership and borrowing system at the memory level
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems
- Formal methods for web security
- System description: lang-n-change -- a tool for transforming languages
- Language definitions as rewrite theories
- From Rewriting Logic, to Programming Language Semantics, to Program Verification
- The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics
Uses Software
This page was built for publication: An overview of the K semantic framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q987974)
