K-Java

DOI10.1145/2676726.2676982zbMath1346.68046OpenAlexW2082036516MaRDI QIDQ2819831

Denis Bogdanas, Grigore Roşu

Publication date: 29 September 2016

Published in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2676726.2676982

zbMATH Keywords

JavaK frameworkmechanized semantics

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (12)

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Towards a trustworthy semantics-based language framework via proof generation ⋮ A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler ⋮ Verifying Reachability-Logic Properties on Rewriting-Logic Specifications ⋮ From Rewriting Logic, to Programming Language Semantics, to Program Verification ⋮ Operationally-based program equivalence proofs using LCTRSs ⋮ Matching µ-logic: Foundation of K framework ⋮ \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages ⋮ A language-independent proof system for full program equivalence ⋮ A Maude environment for CafeOBJ ⋮ On the effectiveness of higher-order logic programming in language-oriented programming ⋮ K-Java

Uses Software

• K Prover

This page was built for publication: K-Java