scientific article; zbMATH DE number 1948157

zbMath1020.03029MaRDI QIDQ4411818

Tobias Nipkow

Publication date: 10 July 2003

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2471/24710103.htm

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (14)

Abstraction and subsumption in modular verification of C programs ⋮ Reasoning About Resources in the Embedded Systems Language Hume ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Verified software units ⋮ A program logic for resources ⋮ Completeness of ASM Refinement ⋮ Completeness of fair ASM refinement ⋮ Relational bytecode correlations ⋮ Certification Using the Mobius Base Logic ⋮ Fifty years of Hoare's logic ⋮ Frame rule for mutually recursive procedures manipulating pointers ⋮ Building program construction and verification tools from algebraic principles ⋮ Relational Decomposition ⋮ Rule-Based Operational Semantics for an Imperative Language

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: