K and KIV: towards deductive verification for arbitrary programming languages

DOI10.1007/978-3-030-73785-6_6MaRDI QIDQ2237340zbMATH OpenOpenAlexFDO

Authors Dominik Klumpp, Philip Lenzen

Publication date 27 October 2021

Full work available at URL https://doi.org/10.1007/978-3-030-73785-6_6

zbMATH Keywords

interactive verificationK frameworkreachability logic

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An overview of the K semantic framework
• Defining and Executing P Systems with Structured Data in K
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)
• K-Java: a complete semantics of Java
• K-Maude: a rewriting based tool for semantics of programming languages
• One-path reachability logic
• Viper: a verification infrastructure for permission-based reasoning
• Why3 -- where programs meet provers

Cited in

(3)

• The WAM case study: Verifying compiler correctness for Prolog with KIV
• Generalising KAT to Verify Weighted Computations
• Deductive verification in decidable fragments with Ivy

Describes a project that uses

Uses Software

• KIV

This page was built for publication: \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2237340)