Conditional Dyck-CFL reachability analysis for complete and efficient library summarization

DOI10.1007/978-3-662-54434-1_33MaRDI QIDQ2988672zbMATH OpenOpenAlexFDO

Authors

Publication date 19 May 2017

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-54434-1_33

Mathematics Subject Classification ID

Theory of programming languages (68N15) Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Summary-based context-sensitive data-dependence analysis in presence of callbacks
• Context-sensitive data-dependence analysis via linear conjunctive language reachability
• Generating precise and concise procedure summaries
• scientific article; zbMATH DE number 1693486
• Loop Summarization and Termination Analysis

Cites work

• scientific article; zbMATH DE number 1693486 (Why is no real title available?)
• scientific article; zbMATH DE number 1956463 (Why is no real title available?)
• scientific article; zbMATH DE number 2087567 (Why is no real title available?)
• scientific article; zbMATH DE number 2090847 (Why is no real title available?)
• Automated inference of library specifications for source-sink property verification
• Conditional must not aliasing for static race detection
• Context-sensitive data-dependence analysis via linear conjunctive language reachability
• Existential Label Flow Inference Via CFL Reachability
• Precise interprocedural dataflow analysis with applications to constant propagation
• Precise interprocedural dataflow analysis with applications to constant propagation
• Specification inference using context-free language reachability
• Summary-based context-sensitive data-dependence analysis in presence of callbacks
• The dependence condition graph: precise conditions for dependence between program points
• Type-base flow analysis

Cited in

(1)

• Accelerating program analyses in Datalog by merging library facts

Describes a project that uses

Uses Software

• Angelic Verification
• SPEC Benchmarks
• SPECjvm2008
• LOCKSMITH

This page was built for publication: Conditional Dyck-CFL reachability analysis for complete and efficient library summarization

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