More Web Proxy on the site http://driver.im/

article

PAGAI: A Path Sensitive Static Analyser

Authors:

David Monniaux,

Matthieu MoyAuthors Info & Claims

Electronic Notes in Theoretical Computer Science (ENTCS), Volume 289

Pages 15 - 25

https://doi.org/10.1016/j.entcs.2012.11.003

Published: 01 December 2012 Publication History

Abstract

We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs.

References

[1]

Bagnara, R., Hill, P.M., Ricci, E. and Zaffanella, E., Precise widening operators for convex polyhedra. Science of Computer Programming. v58 i1-2. 28-56.

[2]

Bagnara, R., Hill, P.M. and Zaffanella, E., The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming. v72 i1-2. 3-21.

[3]

C. Barrett, A. Stump, C. Tinelli, The SMT-LIB Standard: Version 2.0, in: SMT, 2010.

[4]

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Mon niaux, D. and Rival, X., A static analyzer for large safety-critical software. In: Programming Language Design and Implementation (PLDI), ACM. pp. 196-207.

[5]

F. Bourdoncle. Sémantiques des Langages Impératifs d'Ordre Supérieur et Interprétation Abstraite. PhD thesis, ícole Polytechnique, 1992. http://tinyurl.com/BourdonclePhD-pdf.

[6]

Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D. and Rival, X., The ASTRíE analyzer. In: LNCS, number 3444. Springer. pp. 21-30.

[7]

de Moura, L.M. and Bjørner, N., Z3: An efficient SMT solver. In: LNCS, volume 4963. Springer. pp. 337-340.

Digital Library

[8]

Dutertre, B. and de Moura, L.M., A fast linear-arithmetic solver for DPLL(T). In: LNCS, volume 4144. Springer. pp. 81-94.

[9]

Gopan, D. and Reps, T.W., Guided static analysis. In: LNCS, volume 4634. Springer. pp. 349-365.

Digital Library

[10]

Henry, J., Monniaux, D. and Moy, M., Succinct representations for abstract interpretation. In: LNCS,

[11]

Jeannet, B. and Miné, A., Apron: A library of numerical abstract domains for static analysis. In: LNCS, vol. 5643. Springer. pp. 661-667.

[12]

Lattner, C. and Adve, V., LLVM: A compilation framework for lifelong program analysis & transformation. In: IEEE Computer Society, CGO, Washington, DC, USA. pp. 75-86.

[13]

LLVM Language Reference Manual. LLVM team, 2012. http://llvm.org/docs/LangRef.html.

[14]

Symbolic methods to enhance the precision of numerical abstract domains. In: LNCS, volume 3855. Springer. pp. 348-363.

Digital Library

[15]

Monniaux, D. and Gonnord, L., Using bounded model checking to focus fixpoint iterations. In: LNCS, volume 6887. Springer. pp. 369-385.

Digital Library

[16]

http://arxiv.org/abs/1109.2405

Cited By

Arceri VDolcetti GZaffanella E(2024)Speeding up static analysis with the split operatorInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00761-226:5(573-588)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1007/s10009-024-00761-2
Arceri VDolcetti GZaffanella EFerrara PHadarean L(2023)Speeding up Static Analysis with the Split OperatorProceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis10.1145/3589250.3596141(14-19)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3589250.3596141
Lemerre M(2023)SSA Translation Is an Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/35712587:POPL(1895-1924)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571258
Show More Cited By

PAGAI: A Path Sensitive Static Analyser
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Pushdown control-flow analysis for free
POPL '16

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Precise null-pointer analysis

In Java, C or C++, attempts to dereference the null value result in an exception or a segmentation fault. Hence, it is important to identify those program points where this undesired behaviour might occur or prove the other program points (and possibly ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Electronic Notes in Theoretical Computer Science (ENTCS)

Electronic Notes in Theoretical Computer Science (ENTCS) Volume 289, Issue

December, 2012

62 pages

ISSN:1571-0661

Issue’s Table of Contents

Copyright © Elsevier B.V. © 2012.

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 December 2012

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Arceri VDolcetti GZaffanella E(2024)Speeding up static analysis with the split operatorInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00761-226:5(573-588)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1007/s10009-024-00761-2
Arceri VDolcetti GZaffanella EFerrara PHadarean L(2023)Speeding up Static Analysis with the Split OperatorProceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis10.1145/3589250.3596141(14-19)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3589250.3596141
Lemerre M(2023)SSA Translation Is an Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/35712587:POPL(1895-1924)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571258
Arceri VDolcetti GZaffanella E(2023)Unconstrained Variable Oracles for Faster Numeric Static AnalysesStatic Analysis10.1007/978-3-031-44245-2_5(65-83)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44245-2_5
Arceri VMastroeni IZaffanella E(2022)Decoupling the Ascending and Descending Phases in Abstract InterpretationProgramming Languages and Systems10.1007/978-3-031-21037-2_2(25-44)Online publication date: 5-Dec-2022
https://dl.acm.org/doi/10.1007/978-3-031-21037-2_2
Mirliaz SPichardie D(2022)A Flow-Insensitive-Complete Program RepresentationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_10(197-218)Online publication date: 16-Jan-2022
https://dl.acm.org/doi/10.1007/978-3-030-94583-1_10
Alhawi ORocha HGadelha MCordeiro LBatista E(2021)Verification and refutation of C programs based on k-induction and invariant inferenceInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00564-123:2(115-135)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10009-020-00564-1
Votipka DRabin SMicinski KFoster JMazurek MCapkun SRoesner F(2020)An observational investigation of reverse engineers' processesProceedings of the 29th USENIX Conference on Security Symposium10.5555/3489212.3489318(1875-1892)Online publication date: 12-Aug-2020
https://dl.acm.org/doi/10.5555/3489212.3489318
Mallissery SWu YHsieh CBau CHung CCerny TShin DBechini A(2020)Identification of data propagation paths for efficient dynamic information flow trackingProceedings of the 35th Annual ACM Symposium on Applied Computing10.1145/3341105.3373876(92-99)Online publication date: 30-Mar-2020
https://dl.acm.org/doi/10.1145/3341105.3373876
Kim SVenet AThakur A(2020)Memory-Efficient Fixpoint ComputationStatic Analysis10.1007/978-3-030-65474-0_3(35-64)Online publication date: 18-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-65474-0_3
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents