Magic-sets for localised analysis of Java bytecode

DOI10.1007/S10990-010-9063-7MaRDI QIDQ656846zbMATH OpenOpenAlexFDO

Authors Fausto Spoto, Étienne Payet

Publication date 13 January 2012

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://hal.univ-reunion.fr/hal-01186160/file/Magic_sets_for_localised_analysis_of_java_bytecode.pdf

zbMATH Keywords

abstract interpretationstatic analysisdenotational semantics Java byte-codemagic-sets

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• A simple semantics and static analysis for stack inspection
• Sawja: static analysis workshop for Java
• Definite expression aliasing analysis for Java bytecode
• Simple relational correctness proofs for static analyses and program transformations

Cites work

• scientific article; zbMATH DE number 1692935 (Why is no real title available?)
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 1738295 (Why is no real title available?)
• scientific article; zbMATH DE number 1832221 (Why is no real title available?)
• scientific article; zbMATH DE number 1834562 (Why is no real title available?)
• scientific article; zbMATH DE number 5254145 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• Abstract interpretation and application to logic programs
• Bottom-up abstract interpretation of logic programs
• Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
• Class invariants as abstract interpretation of trace semantics
• Constructive versions of Tarski's fixed point theorems
• Efficient goal directed bottom-up evaluation of logic programs
• Graph-Based Algorithms for Boolean Function Manipulation
• Information flow for Algol-like languages
• Magic-sets for localised analysis of Java bytecode
• On the power of magic
• Representing Control: a Study of the CPS Transformation
• Scheme: A interpreter for extended lambda calculus
• Static Analysis
• Two classes of Boolean functions for dependency analysis
• Verification, Model Checking, and Abstract Interpretation

Cited in

(9)

• Certified abstract cost analysis
• Verification, Model Checking, and Abstract Interpretation
• Sawja: static analysis workshop for Java
• Precise Set Sharing Analysis for Java-Style Programs
• Convergence: integrating termination and abort-freedom
• From object fields to local variables: a practical approach to field-sensitive analysis
• Definite expression aliasing analysis for Java bytecode
• scientific article; zbMATH DE number 2018595 (Why is no real title available?)
• Magic-sets for localised analysis of Java bytecode

Describes a project that uses

Uses Software

• PPL
• Boogie
• Groovy
• Cibai

This page was built for publication: Magic-sets for localised analysis of Java bytecode

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