Reasoning in Dynamic Logic about Program Termination

DOI10.1007/978-3-540-78127-1_23zbMath1133.03334OpenAlexW1842068383MaRDI QIDQ5452190

Daniel Leivant

Publication date: 25 March 2008

Published in: Pillars of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78127-1_23

Mathematics Subject Classification ID

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

Related Items (1)

Inductive Completeness of Logics of Programs

Cites Work

• Unnamed Item
• Unnamed Item
• Total correctness in nonstandard logics of programs
• A simple dynamic logic
• A complete logic for reasoning about programs via nonstandard model theory. I
• Hoare's logic and Peano's arithmetic
• First-order dynamic logic
• Termination assertions for recursive programs: Completeness and axiomatic definability
• Arithmetical interpretations of dynamic logic
• Diamond formulas: A fragment of dynamic logic with recursively enumerable validity problem
• Axiomatic Definitions of Programming Languages
• A survey of proof theory

This page was built for publication: Reasoning in Dynamic Logic about Program Termination