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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Boston (1995)
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)
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)
Arntzenius, M., Krishnaswami, N.: Datafun: A functional Datalog. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP) (2016)
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)
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)
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)
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)
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
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)
Cousot, P., et al.: The ASTRÉE analyzer. In: Proceedings of the 14th European Symposium on Programming (ESOP) (2005)
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)
Grädel, E., Tannen, V.: Semiring provenance for first-order model checking (2017). http://arxiv.org/abs/1712.01980
Green, T., Karvounarakis, G., Tannen, V.: Provenance semirings. In: Proceedings of the 26th Symposium on Principles of Database Systems (PODS) (2007)
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)
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)
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)
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)
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)
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)
Livshits, B., et al.: In defense of soundiness: a manifesto. Commun. ACM 58(2), 44–46 (2015)
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)
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)
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)
Manhaeve, R., Dumancic, S., Kimmig, A., Demeester, T., De Raedt, L.: Deepproblog: neural probabilistic logic programming. In: Advances in Neural Information Processing Systems (2018)
Muggleton, S.: Inductive logic programming. New Gener. Comput. 8(4), 295–318 (1991)
Muggleton, S.: Scientific knowledge discovery using inductive logic programming. Commun. ACM 42(11), 42–46 (1999)
Muggleton, S., et al.: ILP turns 20 - biography and future challenges. Mach. Learn. 86(1), 3–23 (2012)
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)
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)
Pearl, J.: Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference. Morgan Kaufmann, Burlington (1988)
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)
Raghothaman, M., Mendelson, J., Zhao, D., Scholz, B., Naik, M.: Provenance-guided synthesis of Datalog programs. Technical report (2019)
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
Richardson, M., Domingos, P.: Markov logic networks. Mach. Learn. 62(1–2), 107–136 (2006)
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)
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)
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)
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)
Zhao, D., Subotic, P., Scholz, B.: Provenance for large-scale Datalog (2019). http://arxiv.org/abs/1907.05045
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
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)