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)
- A rewriting logic semantics approach to modular program analysis
- The rewriting logic semantics project: a progress report
- 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
- Memory representations in rewriting logic semantics definitions
- Dynamic structural operational semantics
- Executable component-based semantics
- A rewriting logic approach to operational semantics
- All-path reachability logic
- 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
- Matching logic
- Matching logic: an alternative to Hoare/Floyd logic
- A truly concurrent semantics for the \(\mathbb{K}\) framework based on graph transformations
- Towards a unified theory of operational and axiomatic semantics
- From hoare logic to matching logic reachability
- Language definitions as rewrite theories
- A Theoretical Foundation for Programming Languages Aggregation
- 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
- 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 Rewriting Logic Approach to Type Inference
- αCheck: A mechanized metatheory model checker
- From rewriting logic, to programming language semantics, to program verification
- Defining and Executing P Systems with Structured Data in K
- Program equivalence by circular reasoning
- A generic framework for symbolic execution: a coinductive approach
- Program logics and their applications
- A rewriting logic approach to operational semantics (extended abstract)
- Formal methods for web security
- K-Maude: a rewriting based tool for semantics of programming languages
- Language definitions as rewrite theories
- Maximally parallel contextual string rewriting
This page was built for software: K Prover
