Before You Code

A Gentle Introduction to Program Analysis

Before diving into OCaml exercises, let's build intuition for what program analysis does,why it matters, and the fundamental tradeoffs every analyzer faces. No coding required — just reading, clicking, and thinking.

Why Program Analysis Matters

On June 4, 1996, the European Space Agency's Ariane 5 rocket exploded 37 seconds after launch. The cause? A software bug that program analysis could have caught.

Timeline of Failure

T+0s

Liftoff. Inertial Reference System (IRS) running guidance software reused from Ariane 4.

T+30s

Software converts 64-bit float (horizontal velocity) to 16-bit signed integer. Ariane 5 is faster than Ariane 4 — the value exceeds 32,767.

T+36s

Integer overflow triggers an Ada exception. The backup IRS — running identical code — also crashes.

T+37s

Flight computer interprets diagnostic data as navigation data, makes a hard turn. Aerodynamic forces tear the rocket apart. Self-destruct activates.

The Actual Bug (Ada Code)

-- Horizontal velocity: ~32,768+ on Ariane 5
-- (was always < 32,767 on Ariane 4)
L_M_BV_32 := TBD.T_ENTIER_16S(BV_Calc_Horiz);
--           ^^^^^^^^^^^^^^^^^
-- Converts 64-bit float to 16-bit signed integer
-- Max value: 32,767 → OVERFLOW!

The conversion had no range check. On Ariane 4, the value was always small enough. On Ariane 5's faster trajectory, it wasn't.

What Program Analysis Would Have Caught

  • ✓Abstract interpretation (interval analysis) would track that BV_Calc_Horiz can exceed 32,767 given Ariane 5's parameters
  • ✓Type range analysis would flag the unchecked 64→16 bit narrowing conversion
  • ✓Astree (a real static analyzer) was later applied to Ariane code and found this exact class of bug automatically

Cost of the bug: $370 million in destroyed rocket + payload. Cost of static analysis: a few hours of compute time.

Your First Static Analysis

Let's walk through how a static analyzer would examine this simple function — step by step, without ever running it.

Step 1/5
1function divide(a, b) {
2  if (b > 0) {
3    return a / b;   // Safe: b is guaranteed > 0
4  } else {
5    return a / b;   // BUG: b could be 0!
6  }
7}
8
9// These calls exist in the program:
10divide(10, 5);    // OK: b=5 > 0, takes true branch
11divide(10, 0);    // BUG: b=0 <= 0, takes false branch → 10/0!
12divide(10, -3);   // OK: b=-3 <= 0, takes false branch → 10/(-3)

Start: Read the function signature

We see `divide(a, b)` takes two parameters. We don't know their values yet — that's the point of static analysis. We reason about ALL possible inputs.

Your First Dynamic Analysis

Now let's analyze the same program dynamically — by actually running it with specific inputs and observing what happens.

1function divide(a, b) {✓
2  if (b > 0) {✓
3    return a / b;✓
4  } else {
5    return a / b;
6  }
7}
Line coverage50%
Input

a=10, b=5

Result

2

b=5 > 0, so we take the true branch (line 3). The false branch (line 5) is never executed. No error — but we only tested one path!

The Fundamental Tradeoff

Every program analysis tool must choose where it sits on the soundness/completeness spectrum. Click each quadrant to learn more.

Soundness vs Completeness 2x2 tradeoff grid: Sound+Complete is impossible (Rice's theorem), Sound+Incomplete includes Astrée and Infer, Unsound+Complete includes Testing and ESLint, Unsound+Incomplete includes pattern matchers

*Rice's theorem: For any non-trivial property of programs, no analyzer can be both sound and complete. This is a fundamental result in computability theory.

Real-World Tools

These tools use the concepts you're learning in this course. Here's what their output actually looks like.

ESLint

static

JavaScript linter — pattern-based static analysis. Fast, unsound, but catches common mistakes.

$ eslint app.js

  3:17  error    'password' is assigned a value but never used  no-unused-vars
  7:5   warning  Unexpected console statement                   no-console
  12:22 error    'getUserById' is not defined                   no-undef
  15:3  warning  'result' is already defined                    no-redeclare
  18:10 error    Expected '===' and instead saw '=='            eqeqeq

✖ 5 problems (3 errors, 2 warnings)
  2 errors and 1 warning potentially fixable with --fix

Ready to Try It Yourself?

You now understand the core ideas behind program analysis. Time to put them into practice.

Analysis Playground

Compare static vs dynamic analysis on 6 different code snippets. See findings, coverage, and Venn diagrams side by side.

Open playground →

Exercise 1: Analysis Comparison

Your first hands-on exercise. Classify analysis techniques, identify tradeoffs, and reason about what different approaches can detect.

Start exercise →