K Prover
From MaRDI portal
Software:43968
No author found.
Source code repository: https://github.com/kframework/k
Related Items (44)
A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Towards a Unified Theory of Operational and Axiomatic Semantics ⋮ A Rewriting Logic Approach to Type Inference ⋮ A Truly Concurrent Semantics for the $\mathbb{K}$ Framework Based on Graph Transformations ⋮ A lazy desugaring system for evaluating programs with sugars ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ Language Definitions as Rewrite Theories ⋮ Verifying Reachability-Logic Properties on Rewriting-Logic Specifications ⋮ From Rewriting Logic, to Programming Language Semantics, to Program Verification ⋮ Logical approximation for program analysis ⋮ The rewriting logic semantics project: a progress report ⋮ Twenty years of rewriting logic ⋮ αCheck: A mechanized metatheory model checker ⋮ Executable component-based semantics ⋮ K-Java ⋮ Program equivalence by circular reasoning ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ Formal methods for web security ⋮ From Hoare Logic to Matching Logic Reachability ⋮ Symbolic execution based on language transformation ⋮ All-Path Reachability Logic ⋮ Memory Representations in Rewriting Logic Semantics Definitions ⋮ K-Maude: A Rewriting Based Tool for Semantics of Programming Languages ⋮ Defining and Executing P Systems with Structured Data in K ⋮ A Theoretical Foundation for Programming Languages Aggregation ⋮ 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 ⋮ Language definitions as rewrite theories ⋮ Matching Logic: An Alternative to Hoare/Floyd Logic ⋮ Implementing type systems for the IDE with Xsemantics ⋮ Unnamed Item ⋮ A rewriting logic approach to operational semantics ⋮ Unnamed Item ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ Maximally Parallel Contextual String Rewriting ⋮ Dynamic structural operational semantics ⋮ Matching Logic ⋮ A Rewriting Logic Semantics Approach to Modular Program Analysis ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract) ⋮ A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters ⋮ 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
This page was built for software: K Prover
