From Rewriting Logic, to Programming Language Semantics, to Program Verification
From MaRDI portal
Publication:2945730
DOI10.1007/978-3-319-23165-5_28zbMath1321.68337OpenAlexW2295221401MaRDI QIDQ2945730
Publication date: 14 September 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-23165-5_28
Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K, Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis, Debugging Maude programs via runtime assertion checking and trace slicing, Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- P systems with control nuclei: the concept
- An overview of the K semantic framework
- 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
- The revised report on the syntactic theories of sequential control and state
- A syntactic approach to type soundness
- Modular structural operational semantics
- A structural approach to operational semantics
- Executable structural operational semantics in Maude
- An Institutional Foundation for the $$\mathbb {K}$$K Semantic Framework
- A Theoretical Foundation for Programming Languages Aggregation
- K-Java
- Language Definitions as Rewrite Theories
- Pragmatics of Modular SOS
- Verified Software Toolchain
- Matching Logic: An Alternative to Hoare/Floyd Logic
- Towards a Unified Theory of Operational and Axiomatic Semantics
- On Abstractions for Timing Analysis in the $\mathbb{K}$ Framework
- A Rewriting Logic Approach to Type Inference
- On the Modular Integration of Abstract Semantics for WCET Analysis
- From Hoare Logic to Matching Logic Reachability
- Collecting Semantics under Predicate Abstraction in the K Framework
- All-Path Reachability Logic
- Defining and Executing P Systems with Structured Data in K
- One-Path Reachability Logic
- Matching Logic - Extended Abstract (Invited Talk)
- Automated Reasoning
- Algebraic Methodology and Software Technology
