Trace-based deductive verification

DOI10.29007/VDFDMaRDI QIDQ7025226zbMATH OpenFDO

Authors Richard Bubel, Dilian Gurov, Reiner Hähnle, Marco Scaletta

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/VDFD

zbMATH Keywords

symbolic executiondeductive verificationcontract based reasoningmu calculustrace contracts

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 3679160 (Why is no real title available?)
• scientific article; zbMATH DE number 1304336 (Why is no real title available?)
• scientific article; zbMATH DE number 1500648 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• -Calculus with Explicit Points and Approximations
• A Hoare logic for the coinductive trace-based big-step semantics of While
• A lattice-theoretical fixpoint theorem and its applications
• A propositional modal logic of time intervals
• An abstract contract theory for programs with procedures
• An axiomatic basis for computer programming
• Deductive software verification: from pen-and-paper proofs to industrial tools
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Locally abstract, globally concrete semantics of concurrent programming languages
• Loop verification with invariants and contracts
• On global induction mechanisms in aμ-calculus with explicit approximations
• Programming Languages and Systems
• Results on the propositional \(\mu\)-calculus
• Separation logic and abstraction
• Sequent calculi for induction and infinite descent
• Temporal abstract interpretation
• Temporal logic with recursion
• Temporal stream logic: synthesis beyond the Bools
• The relationship between separation logic and implicit dynamic frames
• Tightening the contract refinements of a system architecture
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(2)

• History-based reasoning about behavioral subtyping
• History-based reasoning about behavioral subtyping (extended paper)

This page was built for publication: Trace-based deductive verification

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