A Dynamic Logic with Traces and Coinduction

DOI10.1007/978-3-319-24312-2_21zbMath1471.03063OpenAlexW2296215010MaRDI QIDQ3455778

Richard Bubel, Reiner Hähnle, Keiko Nakata, Crystal Chang Din

Publication date: 11 December 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24312-2_21

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Characteristic formulae for liveness properties of non-terminating CakeML programs

Uses Software

• ABS
• KeY-ABS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• KeY-ABS
• KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS
• A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
• “Sometimes” and “not never” revisited
• Dynamic Logic with Trace Semantics
• A Hoare logic for the coinductive trace-based big-step semantics of While
• Programming Languages and Systems
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• A Temporal Dynamic Logic for Verifying Hybrid System Invariants
• Non-termination Checking for Imperative Programs