An abstract interpretation-based model for safety semantics

DOI10.1080/00207161003703205zbMath1215.68125WikidataQ62046216 ScholiaQ62046216MaRDI QIDQ2995468

Roberto Giacobazzi, Isabella Mastroeni

Publication date: 21 April 2011

Published in: International Journal of Computer Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/00207161003703205

zbMATH Keywords

safety; closure operators; semantics; abstract interpretation; program verification

Mathematics Subject Classification ID

68Q70: Algebraic theory of languages and automata

68Q55: Semantics in the theory of computing

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Maximizing entropy over Markov processes

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Grammar semantics, analysis and parsing by abstract interpretation
• Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions
• Defining liveness
• Safety without stuttering
• Recognizing safety and liveness
• Constructive versions of Tarski's fixed point theorems
• Weak relative pseudo-complements of closure operators
• Safety, liveness and fairness in temporal logic
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• Grammar Analysis and Parsing by Abstract Interpretation
• Countable nondeterminism and random assignment
• Proving Liveness Properties of Concurrent Programs
• Guarded commands, nondeterminacy and formal derivation of programs
• Proving the Correctness of Multiprocess Programs
• Refining and compressing abstract domains
• Systematic design of program transformation frameworks by abstract interpretation
• Making abstract interpretations complete
• An axiomatic basis for computer programming