Is Program Analysis The Silver Bullet Against Software Bugs?

Program analysis is the art of reasoning about the run-time behavior of a program without necessarily executing it. This information is useful for various real-life applications such as supporting software developers (e.g., bug-finding tools, code refactoring tools, and code recommenders) and compiler optimizations. Program analysis is also used to ensure complex software adheres to standards and regulations (e.g., medical devices, car industry, and aviation industry).

In this talk, I will discuss the three main properties that enable program analyses to be useful in practice: scalability, precision, and usability. I will relate that to various papers that have been published in the field of program analysis, as well as some of the work that my group has done. I will conclude with where I see program analysis research going and the challenges that we aim to solve in the field.

References

• Strictly declarative specification of sophisticated points-to analyses by Martin Bravenboer and Yannis Smaragdakis
• Dimensions of Precision in Reference Analysis of Object-Oriented Programming Languages by Barbara G. Ryder
• Averroes: Whole-Program Analysis without the Whole Program by Karim Ali and Ondřej Lhoták
• FlowDroid: Precise Context, Flow, Field, Object-Sensitive and Lifecycle-Aware Taint Analysis for Android Apps by Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel
• Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation by Shmuel Sagiv, Thomas W. Reps, and Susan Horwitz
• Context-, Flow-, and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems by Johannes Späth, Karim Ali, and Eric Bodden
• Debugging Static Analysis by Lisa Nguyen Quang Do, Stefan Krüger, Patrick Hill, Karim Ali, and Eric Bodden
• Towards Better Inlining Decisions Using Inlining Trials by Jeffrey Dean and Craig Chamber
• Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks by Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer
• Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification by Pengfei Yang, Jiangchao Liu, Jianlin Li, Liqian Chen, and Xiaowei Huang
• Soot
• IBM. T.J. Watson Libraries for Analysis WALA

Karim Ali is an Assistant Professor in the Department of Computing Science at the University of Alberta. His research interests are in programming languages and software engineering, particularly in scalability, precision, and usability of program analysis tools. His work ranges from developing new theories for scalable and precise program analyses to applications of program analysis in security and Just-in-Time compilers.

Karim obtained his PhD degree from the University of Waterloo in 2014, and was a postdoctoral research at Technische Universität Darmstadt (TU Darmstadt) 2014–2016.

• Twitter @karimhamdanali
• Site: https://karimali.ca/
• DBLP: https://dblp.org/pers/hd/a/Ali_0001:Karim