Liminf progress measures

DOI10.1007/3-540-55511-0_25MaRDI QIDQ6171780zbMATH OpenOpenAlexFDO

Authors Nils Klarlund

Publication date 16 August 2023

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

Full work available at URL https://doi.org/10.1007/3-540-55511-0_25

Mathematics Subject Classification ID

Descriptive set theory (03E15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Improvement in small progress measures
• Towards Lim
• Measures
• Progress under bounded fairness

Cites work

• A proof rule for fair termination of guarded commands
• Adequate proof principles for invariance and liveness properties of concurrent programs
• An axiomatic basis for computer programming
• Countable nondeterminism and random assignment
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Decision problems forω-automata
• Descriptive set theory
• Fair termination revisited - with delay
• scientific article; zbMATH DE number 3965428 (Why is no real title available?)
• scientific article; zbMATH DE number 3972158 (Why is no real title available?)
• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 17700 (Why is no real title available?)
• scientific article; zbMATH DE number 1354159 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Infinite trees, markings, and well-foundedness
• Metric interpretations of infinite trees and semantics of non deterministic recursive programs
• Progress measures and stack assertions for fair termination
• Proof rules and transformations dealing with fairness
• Recognizing safety and liveness
• Temporal logic can be more expressive
• Ten Years of Hoare's Logic: A Survey—Part I
• The \(\mu\)-calculus as an assertion-language for fairness arguments
• The existence of refinement mappings
• Verification of concurrent programs: The automata-theoretic framework
• Verifying temporal properties without temporal logic

Cited in

(1)

• Solving mean-payoff games via quasi dominions

This page was built for publication: Liminf progress measures

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