Rust NYC: Scalable static analysis: confronting the halting problem

Join us on Wednesday, October 29th at Materialize. Doors open at 6:30 p.m. to give attendees plenty of time to grab pizza and socialize, and the talk begin at 7:30 p.m.

Kristopher Micinski — Assistant professor at Syracuse — Scalable static analysis: confronting the halting problem

Program analysis asks the question "what might this program possibly do?" A definitive answer to this question is impossible due to the halting problem: it is even undecidable to say whether any given line of code is definitely reached. Thus, all program analyses inexorably grapple with challenging trade-offs between complexity, tractability, correctness, and usefulness. Balancing all of these concerns, while also ensuring a scalable implementation (in expressivity, language feature set, parallelization, etc.) is a seriously challenging task, especially given that even constructing a correct analysis is challenging enough on its own.
In this talk, I will give a whirlwind introduction to state-of-the-art techniques used to deploy state-of-the-art scalable static analysis engines for production software systems. I will focus on the core theories apropos to program analysis (abstract interpretation, lattices, monotonic functions, fixed points, etc.), but will complement the theory by grounding my presentation in a discussion of relevant implementation details (particularly in Ascent, a high-performance Rust-embedded Datalog compiler). I will close by discussing some of our work in scaling program analyses on high-performance GPU clusters, analyzing >1M-line codebases at the highest possible scale on modern hardware.

---

Kristopher Micinski is an (assistant) professor at Syracuse. He works on highly-scalable program analysis, analytic reasoning, and deductive databases. He is especially interested in Datalog, a chain-forward language that has some desirable properties in the context of high-performance static analysis design. His students have currently built the fastest Datalog engines on CPUs, GPUs, and supercomputing clusters. In his spare time he works on woodworking

kmicinski.com
https://types.pl/@krismicinski

Lawrence Harvey is Rust NYC's official recruitment partner, with Ross providing support as a co-organizer and financial support.

The space is generously sponsored by our longstanding partner Materialize.