6 posts
How to run formal static analysis in your CI pipeline using Infer, with working configs and realistic trade-offs.
Abstract interpretation is the kind of term that makes engineers close the tab. It sounds like something you need a semester of lattice theory to understand.…
Large language models can help triage static analysis false positives, but they don't understand program semantics the way abstract interpretation does.
Your static analyzer just emitted 847 warnings on a Friday afternoon. You know, statistically, that somewhere between 5% and 15% of them are real bugs. The…
How Facebook used abstract interpretation and intentional unsoundness to find race conditions at scale in millions of lines of Android code.
Facebook's Android app had a performance problem. The UI thread was drowning in work, but moving code to background threads meant race conditions. Crashes in…
Meta's Infer uses abstract interpretation and bi-abduction to find null dereferences, memory leaks, and race conditions by reasoning about code structure,...
Meta has shipped over 100,000 bug fixes that were caught by a static analyzer before the code ever reached a user. The tool is called Infer, it is open source,…
Abstract interpretation over-approximates every possible program state.
Static analysis cannot prove an airplane will not crash. It can prove that your altimeter control loop will never divide by zero, will never index out of…
Abstract interpretation lets you prove runtime errors impossible before execution.
Your test suite passes. Your type checker is green. You ship. Two hours later, production throws an on an edge case no one thought to test. Testing finds bugs.…