Sawja: static analysis workshop for Java

DOI10.1007/978-3-642-18070-5_7MaRDI QIDQ3067538zbMATH OpenOpenAlexWikidataFDO

Authors

Publication date 21 January 2011

Published in Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.3353

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when developing a full-fledged analyzer for a realistic language such as Java. This paper describes the Sawja library: a static analysis framework fully compliant with Java 6 which provides OCaml modules for efficiently manipulating Java bytecode programs. We present the main features of the library, including (i) efficient functional data-structures for representing program with implicit sharing and lazy parsing, (ii) an intermediate stack-less representation, and (iii) fast computation and manipulation of complete programs.

Recommendations

• Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
• scientific article; zbMATH DE number 1617328
• Rewriting Approximations for Fast Prototyping of Static Analyzers
• Computer Aided Verification
• Magic-sets for localised analysis of Java bytecode

Cites work

• scientific article; zbMATH DE number 1122098 (Why is no real title available?)
• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• scientific article; zbMATH DE number 1956463 (Why is no real title available?)
• Interacting with Modal Logics in the Coq Proof Assistant
• Lightweight bytecode verification
• On programming of arithmetic operations
• Programming Languages and Systems
• Secure the clones. Static enforcement of policies for secure object copying

Cited in

(6)

• Sawja
• Hash consed points-to sets
• A flow-insensitive-complete program representation
• ProMoVer: modular verification of temporal safety properties
• Programming Languages and Systems
• Magic-sets for localised analysis of Java bytecode

Describes a project that uses

Uses Software

• ASTREE
• OCaml
• WALA
• Soot
• Coq
• PATRICIA
• Barista

This page was built for publication: Sawja: static analysis workshop for Java

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