From rewriting logic, to programming language semantics, to program verification
From MaRDI portal
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
Cites work
- A rewriting logic approach to operational semantics
- A Rewriting Logic Approach to Type Inference
- A structural approach to operational semantics
- A syntactic approach to type soundness
- A Theoretical Foundation for Programming Languages Aggregation
- Algebraic Methodology and Software Technology
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- An Institutional Foundation for the $$\mathbb {K}$$K Semantic Framework
- An overview of the K semantic framework
- Automated Reasoning
- Collecting Semantics under Predicate Abstraction in the K Framework
- Conditional rewriting logic as a unified model of concurrency
- Defining and Executing P Systems with Structured Data in K
- Executable structural operational semantics in Maude
- From hoare logic to matching logic reachability
- scientific article; zbMATH DE number 4035108 (Why is no real title available?)
- scientific article; zbMATH DE number 49477 (Why is no real title available?)
- scientific article; zbMATH DE number 1418328 (Why is no real title available?)
- scientific article; zbMATH DE number 7149819 (Why is no real title available?)
- K-Java: a complete semantics of Java
- Language definitions as rewrite theories
- Matching logic -- extended abstract (invited talk)
- Matching logic: an alternative to Hoare/Floyd logic
- Modular rewriting semantics in practice
- Modular structural operational semantics
- On Abstractions for Timing Analysis in the $\mathbb{K}$ Framework
- On the modular integration of abstract semantics for WCET analysis
- One-path reachability logic
- P systems with control nuclei: the concept
- Pragmatics of modular SOS
- The chemical abstract machine
- The revised report on the syntactic theories of sequential control and state
- Towards a unified theory of operational and axiomatic semantics
- Verified software toolchain (invited talk)
Cited in
(13)- scientific article; zbMATH DE number 1617312 (Why is no real title available?)
- Combining runtime checking and slicing to improve Maude error diagnosis
- Mechanized semantics
- The rewriting logic semantics project: a progress report
- Declarative Semantics for Revision Programming and Connections to Active Integrity Constraints
- The rewriting logic semantics project: a progress report
- Program logics and their applications
- Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
- From process logic to program logic
- From program verification to program synthesis
- A rewriting logic semantics approach to modular program analysis
- Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K
- Debugging Maude programs via runtime assertion checking and trace slicing
Describes a project that uses
Uses Software
This page was built for publication: From rewriting logic, to programming language semantics, to program verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945730)
