K Prover
From MaRDI portal
Software:43968
swMATH32257MaRDI QIDQ43968FDOQ43968
Author name not available (Why is that?)
Source code repository: https://github.com/kframework/k
Cited In (44)
- 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
- A rewriting logic approach to operational semantics
- Maximally Parallel Contextual String Rewriting
- 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
- K-Java: a complete semantics of Java
- P systems with control nuclei: the concept
- Operational semantics of a weak memory model with channel synchronization
- Symbolic execution based on language transformation
- A Theoretical Foundation for Programming Languages Aggregation
- Title not available (Why is that?)
- 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
- K-Maude: A Rewriting Based Tool for Semantics of Programming Languages
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Logical approximation for program analysis
- A lazy desugaring system for evaluating programs with sugars
- A rewrite framework for language definitions and for generation of efficient interpreters
- A Truly Concurrent Semantics for the $\mathbb{K}$ Framework Based on Graph Transformations
- Matching Logic: An Alternative to Hoare/Floyd Logic
- The Rewriting Logic Semantics Project: A Progress Report
- Towards a Unified Theory of Operational and Axiomatic Semantics
- A Rewriting Logic Approach to Type Inference
- αCheck: A mechanized metatheory model checker
- A Rewriting Logic Semantics Approach to Modular Program Analysis
- Defining and Executing P Systems with Structured Data in K
- Memory Representations in Rewriting Logic Semantics Definitions
- Program equivalence by circular reasoning
- A generic framework for symbolic execution: a coinductive approach
- All-Path Reachability Logic
- A rewriting logic approach to operational semantics (extended abstract)
- Matching Logic
- From Hoare Logic to Matching Logic Reachability
- Formal methods for web security
- Language Definitions as Rewrite Theories
- Language definitions as rewrite theories
- From Rewriting Logic, to Programming Language Semantics, to Program Verification
This page was built for software: K Prover
