An overview of the K semantic framework

DOI10.1016/J.JLAP.2010.03.012zbMATH1214.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

zbMATH Keywords

concurrent languagesrewrite rules

Mathematics Subject Classification ID

Theory of programming languages (68N15) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

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

Cites work

• scientific article; zbMATH DE number 4074517 (Why is no real title available?)
• scientific article; zbMATH DE number 3633737 (Why is no real title available?)
• scientific article; zbMATH DE number 5051639 (Why is no real title available?)
• A Rewriting Logic Approach to Type Inference
• A rewrite framework for language definitions and for generation of efficient interpreters
• A rewriting logic approach to operational semantics
• A structural approach to operational semantics
• A syntactic approach to type soundness
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Automated Reasoning
• Computer Aided Verification
• Computing with membranes
• Conditional rewriting logic as a unified model of concurrency
• Defining and Executing P Systems with Structured Data in K
• Formal methods for open object-based distributed systems. 9th IFIP WG 6.1 international conference FMOODS 2007, Paphos, Cyprus, June 6--8, 2007. Proceedings.
• MGS: a rule-based programming language for complex objects and collections
• Membrane systems with promoters/inhibitors
• Modular structural operational semantics
• Pragmatics of modular SOS
• Rewriting logic as a semantic framework for concurrency: a progress report
• The chemical abstract machine
• The gamma model and its discipline of programming
• The power of communication: P systems with symport/antiport
• The rewriting logic semantics project

Cited in

(45)

• Transforming concurrent programs with semaphores into logically constrained term rewrite systems
• Formally verified animation for RoboChart using interaction trees
• \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
• Program equivalence by circular reasoning
• Executable component-based semantics
• On the effectiveness of higher-order logic programming in language-oriented programming
• The rewriting logic semantics project: a progress report
• A lazy desugaring system for evaluating programs with sugars
• The rewriting logic semantics project: a progress report
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Dynamic structural operational semantics
• 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
• Matching logic: an alternative to Hoare/Floyd logic
• A generic framework for symbolic execution: a coinductive approach
• A framework for modeling the semantics of synchronous and asynchronous procedures with abstract state machines
• P systems with control nuclei: the concept
• Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K
• Towards a \(\mathbb{K}\)ool future
• System description: lang-n-change -- a tool for transforming languages
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• Language definitions as rewrite theories
• Symbolic execution based on language transformation
• A truly concurrent semantics for the \(\mathbb{K}\) framework based on graph transformations
• Implementing type systems for the IDE with Xsemantics
• A calculus for language transformations
• Operational semantics of a weak memory model with channel synchronization
• Collecting Semantics under Predicate Abstraction in the K Framework
• Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
• K Prover
• αCheck: A mechanized metatheory model checker
• From rewriting logic, to programming language semantics, to program verification
• A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
• Maximally parallel contextual string rewriting
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• Operational semantics of a weak memory model with channel synchronization
• scientific article; zbMATH DE number 7204429 (Why is no real title available?)
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Formal methods for web security
• Defining and Executing P Systems with Structured Data in K
• Twenty years of rewriting logic
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics
• Formally understanding Rust's ownership and borrowing system at the memory level

Describes a project that uses

Uses Software

• ML
• JavaFAN
• OBJ3
• Maude
• K-Maude
• MGS
• KOOL

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)