\( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages

DOI10.1007/978-3-030-73785-6_6OpenAlexW3156605414MaRDI QIDQ2237340

Philip Lenzen, Dominik Klumpp

Publication date: 27 October 2021

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

zbMATH Keywords

reachability logicinteractive verificationK framework

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• KIV

Cites Work

• An overview of the K semantic framework
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• K-Java
• K-Maude: A Rewriting Based Tool for Semantics of Programming Languages
• All-Path Reachability Logic
• Defining and Executing P Systems with Structured Data in K
• One-Path Reachability Logic
• Why3 — Where Programs Meet Provers
• Unnamed Item

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