K Prover
From MaRDI portal
swMATH32257MaRDI QIDQ43968FDOQ43968
Author name not available (Why is that?)
Official website: http://www.kframework.org/index.php/Main_Page
Source code repository: https://github.com/kframework/k
Cited In (only showing first 100 items - show all)
- Title not available (Why is that?)
- KtoIsabelle
- Memory representations in rewriting logic semantics definitions
- Dynamic structural operational semantics
- 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
- 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
- Logical approximation for program analysis
- A lazy desugaring system for evaluating programs with sugars
- αCheck: A mechanized metatheory model checker
- A rewriting logic approach to operational semantics (extended abstract)
- LambdaMu-calculus
- eThor
- 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
- Twenty years of rewriting logic
- Executable component-based semantics
- A rewriting logic approach to operational semantics
- K-Java: a complete semantics of Java
- P systems with control nuclei: the concept
- 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
- 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
- Ott
- Stratego
- JavaFAN
- CoqJVM
- TinkerType
- ITP/OCL
- LOGEN
- OBJ3
- Rascal
- CIRC
- CafeOBJ
- Maude
- 2OBJ
- Agapia
- ATGen
- MMT
- TRACER
- PVeStA
- Lem
- Cyclone
- SOCLE
- K tool
- K-Maude
- Dist-Orc
- PLT Redex
- Toolchain
- MOMENT2
- Tom
- TSOTool
- vlogsl
- Mezzo
- PrologCheck
- CoDeSe
- TS#
- Spoofax
- A rewrite framework for language definitions and for generation of efficient interpreters
- LCLint
- K-Java
- KJS
- SymPLFIED
- XASM
- MGS
- Alms
- KLOVERA
- JavAdaptor
- JSLINQ
- BicolanoMT
- Hackage
- Jinja Threads
- SeLINQ
- coFJ
- Centaur
- CLDC
- Java+ITP
- KOOL
- SILF
- Ruler
- A Rewriting Logic Approach to Type Inference
- TSL
- 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
- Formal methods for web security
This page was built for software: K Prover
