Class invariants as abstract interpretation of trace semantics

DOI10.1016/j.cl.2005.01.001zbMath1387.68052OpenAlexW1967714136MaRDI QIDQ1749225

Francesco Logozzo

Publication date: 16 May 2018

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cl.2005.01.001

zbMATH Keywords

verificationoptimizationstatic analysisobject-oriented programmingabstract interpretationtrace semanticsclass invariance

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items

Relational string abstract domains, Magic-sets for localised analysis of Java bytecode, Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes, An operational semantics for object-oriented concepts based on the class hierarchy

Uses Software

• LARCH
• Eiffel
• JML
• ESC/Java
• ASTREE
• Featherweight Java
• Houdini

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A lattice-theoretical fixpoint theorem and its applications
• Abstract Interpretation Frameworks
• Algebraic Methodology and Software Technology
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation