Skip to main content
SpringerLink
Log in

Rethinking Static Analysis by Combining Discrete and Continuous Reasoning

  • Conference paper
  • First Online:
Static Analysis (SAS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11822))

Included in the following conference series:

  • 726 Accesses

Abstract

Static analyses predominantly use discrete modes of logical reasoning to derive facts about programs. Despite significant strides, this form of reasoning faces new challenges in modern software applications and practices. These challenges concern not only traditional analysis objectives such as scalability, accuracy, and soundness, but also emerging ones such as tailoring analysis conclusions based on relevance or severity of particular code changes, and needs of individual programmers.

We advocate seamlessly extending static analyses to leverage continuous modes of logical reasoning in order to address these challenges. Central to our approach is expressing the specification of the static analysis in a constraint language that is amenable to computing provenance information. We use the logic programming language Datalog as proof-of-concept for this purpose. We illustrate the benefits of exploiting provenance even in the discrete setting. Moreover, by associating weights with constraints, we show how to amplify these benefits in the continuous setting.

We also present open problems in aspects of analysis usability, language expressiveness, and solver techniques. The overall process constitutes a fundamental rethinking of how to design, implement, deploy, and adapt static analyses.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Boston (1995)

    MATH  Google Scholar 

  2. Albarghouthi, A., Koutris, P., Naik, M., Smith, C.: Constraint-based synthesis of Datalog programs. In: Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP) (2017)

    Google Scholar 

  3. Aref, M., et al.: Design and implementation of the LogicBlox system. In: Proceedings of the ACM SIGMOD International Conference on Management of Data (SIGMOD) (2015)

    Google Scholar 

  4. Arntzenius, M., Krishnaswami, N.: Datafun: A functional Datalog. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP) (2016)

    Google Scholar 

  5. Avgustinov, P., de Moor, O., Jones, M.P., Schäfer, M.: QL: Object-oriented queries on relational data. In: Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP) (2016)

    Google Scholar 

  6. Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2002)

    Google Scholar 

  7. Bessey, A., et al.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66–75 (2010)

    Article  Google Scholar 

  8. Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: Proceedings of the ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA) (2009)

    Google Scholar 

  9. Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_1

    Chapter  Google Scholar 

  10. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (1977)

    Google Scholar 

  11. Cousot, P., et al.: The ASTRÉE analyzer. In: Proceedings of the 14th European Symposium on Programming (ESOP) (2005)

    Chapter  Google Scholar 

  12. De Raedt, L., Kimmig, A., Toivonen, H.: Problog: A probabilistic Prolog and its application in link discovery. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (2007)

    Google Scholar 

  13. Grädel, E., Tannen, V.: Semiring provenance for first-order model checking (2017). http://arxiv.org/abs/1712.01980

  14. Green, T., Karvounarakis, G., Tannen, V.: Provenance semirings. In: Proceedings of the 26th Symposium on Principles of Database Systems (PODS) (2007)

    Google Scholar 

  15. Grigore, R., Yang, H.: Abstraction refinement guided by a learnt probabilistic model. In: Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2016)

    Google Scholar 

  16. Heo, K., Raghothaman, M., Si, X., Naik, M.: Continuously reasoning about programs using differential bayesian inference. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2019)

    Google Scholar 

  17. Hoder, K., Bjørner, N., De Moura, L.: \(\mu \)z: An efficient engine for fixed points with constraints. In: Proceedings of the 23rd International Conference on Computer-Aided Verification (CAV) (2011)

    Google Scholar 

  18. Kimmig, A., den Broeck, G.V., De Raedt, L.: An algebraic Prolog for reasoning about possible worlds. In: Proceedings of the 25th AAAI Conference on Artificial Intelligence (2011)

    Google Scholar 

  19. Lahiri, S., Vaswani, K., Hoare, C.A.R.: Differential static analysis: opportunities, applications, and challenges. In: Proceedings of the FSE/SDP Workshop on Future of Software Engineering Research (FoSER) (2010)

    Google Scholar 

  20. Lee, W., Lee, W., Yi, K.: Sound non-statistical clustering of static analysis alarms. In: Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) (2012)

    Google Scholar 

  21. Livshits, B., et al.: In defense of soundiness: a manifesto. Commun. ACM 58(2), 44–46 (2015)

    Article  Google Scholar 

  22. Madsen, M., Yee, M.H., Lhoták, O.: From datalog to Flix: a declarative language for fixed points on lattices. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2016)

    Google Scholar 

  23. Mangal, R., Zhang, X., Naik, M., Nori, A.V.: Volt: A lazy grounding framework for solving very large MaxSAT instances. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT) (2015)

    Google Scholar 

  24. Mangal, R., Zhang, X., Nori, A., Naik, M.: A user-guided approach to program analysis. In: Proceedings of the Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) (2015)

    Google Scholar 

  25. Manhaeve, R., Dumancic, S., Kimmig, A., Demeester, T., De Raedt, L.: Deepproblog: neural probabilistic logic programming. In: Advances in Neural Information Processing Systems (2018)

    Google Scholar 

  26. Muggleton, S.: Inductive logic programming. New Gener. Comput. 8(4), 295–318 (1991)

    Article  Google Scholar 

  27. Muggleton, S.: Scientific knowledge discovery using inductive logic programming. Commun. ACM 42(11), 42–46 (1999)

    Article  Google Scholar 

  28. Muggleton, S., et al.: ILP turns 20 - biography and future challenges. Mach. Learn. 86(1), 3–23 (2012)

    Article  MathSciNet  Google Scholar 

  29. Naik, M., Aiken, A., Whaley, J.: Effective static race detection for Java. In: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2006)

    Google Scholar 

  30. O’Hearn, P.W.: Continuous reasoning: scaling the impact of formal methods. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2018)

    Google Scholar 

  31. Pearl, J.: Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference. Morgan Kaufmann, Burlington (1988)

    MATH  Google Scholar 

  32. Raghothaman, M., Kulkarni, S., Heo, K., Naik, M.: User-guided program reasoning using Bayesian inference. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2018)

    Google Scholar 

  33. Raghothaman, M., Mendelson, J., Zhao, D., Scholz, B., Naik, M.: Provenance-guided synthesis of Datalog programs. Technical report (2019)

    Google Scholar 

  34. Reps, T.: Demand interprocedural program analysis using logic databases. In: Ramakrishnan, R. (ed.) Applications of Logic Databases, vol. 296. Springer, Boston (1995). https://doi.org/10.1007/978-1-4615-2207-2_8

    Chapter  Google Scholar 

  35. Richardson, M., Domingos, P.: Markov logic networks. Mach. Learn. 62(1–2), 107–136 (2006)

    Article  Google Scholar 

  36. Si, X., Raghothaman, M., Heo, K., Naik, M.: Synthesizing Datalog programs using numerical relaxation. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI) (2019)

    Google Scholar 

  37. Xu, J., Zhang, W., Alawini, A., Tannen, V.: Provenance analysis for missing answers and integrity repairs. IEEE Data Eng. Bull. 41(1), 39–50 (2018)

    Google Scholar 

  38. Zhang, X., Grigore, R., Si, X., Naik, M.: Effective interactive resolution of static analysis alarms. In: Proceedings of the ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications (OOPSLA) (2017)

    Google Scholar 

  39. Zhang, X., Mangal, R., Grigore, R., Naik, M., Yang, H.: On abstraction refinement for program analyses in Datalog. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2014)

    Google Scholar 

  40. Zhao, D., Subotic, P., Scholz, B.: Provenance for large-scale Datalog (2019). http://arxiv.org/abs/1907.05045

Download references

Acknowledgments

I thank the following for making vital contributions to the body of research summarized in this paper: PhD students Sulekha Kulkarni, Xujie Si, and Xin Zhang; postdocs Kihong Heo, Woosuk Lee, and Mukund Raghothaman; and collaborators Radu Grigore, Aditya Nori, and Hongseok Yang. I am grateful to Peter O’Hearn for providing useful feedback at various stages of this work. This research was supported by DARPA award #FA8750-15-2-0009, NSF awards #1253867 and #1526270, ONR award #N00014-18-1-2021, and gifts from Facebook, Google, and Microsoft.

Author information

Authors and Affiliations

  1. Department of Computer and Information Science, University of Pennsylvania, Philadelphia, USA

    Mayur Naik

Authors
  1. Mayur Naik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mayur Naik .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, CO, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Naik, M. (2019). Rethinking Static Analysis by Combining Discrete and Continuous Reasoning. In: Chang, BY. (eds) Static Analysis. SAS 2019. Lecture Notes in Computer Science(), vol 11822. Springer, Cham. https://doi.org/10.1007/978-3-030-32304-2_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32304-2_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32303-5

  • Online ISBN: 978-3-030-32304-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation