An abstract interpretation-based model for safety semantics

DOI10.1080/00207161003703205MaRDI QIDQ2995468zbMATH OpenOpenAlexWikidataFDO

Authors Isabella Mastroeni, Roberto Giacobazzi

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

semanticsabstract interpretationprogram verificationsafetyclosure operators

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Algebraic theory of languages and automata (68Q70) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 176726
• Reactive safety
• Calculational design of a regular model checker by abstract interpretation
• A lattice-theoretic characterization of safety and liveness
• Property directed abstract interpretation

Cites work

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

Cited in

(9)

• The meaning of memory safety
• Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation
• Calculational design of a regular model checker by abstract interpretation
• Maximizing entropy over Markov processes
• Undecidability of safety for the schematic protection model with cyclic creates
• An efficient abstract machine for safe ambients
• A Revised Concept of Safety for General Answer Set Programs
• scientific article; zbMATH DE number 176726 (Why is no real title available?)
• scientific article; zbMATH DE number 1107560 (Why is no real title available?)

This page was built for publication: An abstract interpretation-based model for safety semantics

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