An overview of the K semantic framework

DOI10.1016/j.jlap.2010.03.012zbMath1214.68188OpenAlexW2048417351MaRDI QIDQ987974

Grigore Roşu, Traian-Florin Ş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) Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42)

Related Items

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K ⋮ A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler ⋮ A lazy desugaring system for evaluating programs with sugars ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ Verifying Reachability-Logic Properties on Rewriting-Logic Specifications ⋮ From Rewriting Logic, to Programming Language Semantics, to Program Verification ⋮ The rewriting logic semantics project: a progress report ⋮ Twenty years of rewriting logic ⋮ Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ αCheck: A mechanized metatheory model checker ⋮ The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics ⋮ Formally verified animation for RoboChart using interaction trees ⋮ A Calculus for Language Transformations ⋮ Executable component-based semantics ⋮ Program equivalence by circular reasoning ⋮ \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ Formal methods for web security ⋮ Symbolic execution based on language transformation ⋮ All-Path Reachability Logic ⋮ P systems with control nuclei: the concept ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ Language definitions as rewrite theories ⋮ Matching Logic: An Alternative to Hoare/Floyd Logic ⋮ On the effectiveness of higher-order logic programming in language-oriented programming ⋮ System description: lang-n-change -- a tool for transforming languages ⋮ Implementing type systems for the IDE with Xsemantics ⋮ Unnamed Item ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ K Prover ⋮ Maximally Parallel Contextual String Rewriting ⋮ Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework ⋮ Dynamic structural operational semantics ⋮ Model checking of synchronized domain-specific multi-formalism models using high-level Petri nets ⋮ A framework for modeling the semantics of synchronous and asynchronous procedures with abstract state machines ⋮ Pattern eliminating transformations

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The power of communication: P systems with symport/antiport
• The gamma model and its discipline of programming
• The rewriting logic semantics project
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• A rewriting logic approach to operational semantics
• Conditional rewriting logic as a unified model of concurrency
• The chemical abstract machine
• A syntactic approach to type soundness
• Membrane systems with promoters/inhibitors
• Computing with membranes
• Modular structural operational semantics
• A structural approach to operational semantics
• 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 Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters
• Pragmatics of Modular SOS
• A Rewriting Logic Approach to Type Inference
• Defining and Executing P Systems with Structured Data in K
• Automated Reasoning
• Computer Aided Verification
• Rewriting logic as a semantic framework for concurrency: a progress report