Invariant detection is the process of automatically discovering properties that always hold during program execution — identifying relationships between variables, data structures, and program states that remain true across all observed executions, providing insights into program behavior and enabling verification, testing, and debugging.

What Is an Invariant?

• Invariant: A property or condition that is always true at a specific program point.
• Examples:
• array_size >= 0 — size is never negative
• balance >= 0 — bank balance is non-negative
• left <= right — in binary search, left pointer never exceeds right
• size == elements.length — size field matches actual array length

Why Detect Invariants?

• Program Understanding: Invariants reveal implicit assumptions and constraints in code.
• Documentation: Automatically document program properties without manual effort.
• Bug Detection: Violations of invariants indicate bugs.
• Verification: Invariants are essential for formal verification — proving correctness requires knowing what properties should hold.
• Test Generation: Use invariants to generate valid test inputs and check test outputs.

How Invariant Detection Works

1. Instrumentation: Insert probes into the program to log variable values at key points (function entry/exit, loop headers, etc.).

2. Execution: Run the program on test inputs, collecting traces of variable values.

3. Candidate Generation: Generate candidate invariants — hypotheses about properties that might hold.

4. Filtering: Check candidates against observed traces — discard those that are violated.

5. Reporting: Present likely invariants to developers — those that held in all observed executions.

Types of Invariants

• Unary Invariants: Properties of single variables.
• x > 0 — x is always positive
• x != null — x is never null
• x in {1, 2, 3} — x is always one of these values

• Binary Invariants: Relationships between two variables.
• x < y — x is always less than y
• x == y + 1 — x is always one more than y
• x == y * 2 — x is always twice y

• Array Invariants: Properties of arrays or sequences.
• arr[i] <= arr[i+1] — array is sorted
• all elements are non-negative
• no duplicates

• Object Invariants: Properties of object state.
• this.size == this.elements.length
• this.head != null implies this.size > 0

• Temporal Invariants: Properties about execution order.
• open() always called before read()
• lock() and unlock() are balanced

Daikon: The Classic Invariant Detector

• Daikon is the most well-known invariant detection tool.
• Process:

1. Instrument Java/C/C++ programs to log variable values. 2. Run instrumented program on test suite. 3. Analyze traces to find invariants.

Example: Daikon in Action

public class BankAccount {
    private double balance;
    private int transactionCount;
    
    public void deposit(double amount) {
        balance += amount;
        transactionCount++;
    }
    
    public void withdraw(double amount) {
        if (balance >= amount) {
            balance -= amount;
            transactionCount++;
        }
    }
}

// Daikon detects invariants:
// - balance >= 0  (always non-negative)
// - transactionCount >= 0  (always non-negative)
// - transactionCount increases monotonically
// - After deposit: balance == old(balance) + amount
// - After withdraw: balance == old(balance) - amount OR balance == old(balance)

Invariant Templates

• Daikon uses templates to generate candidate invariants:
• x == a (constant)
• x > a, x >= a, x < a, x <= a (bounds)
• x == y, x != y (equality)
• x < y, x <= y (ordering)
• x == y + a (linear relationship)
• x == y * a (multiplicative relationship)
• x in {a, b, c} (enumeration)

Statistical Confidence

• Problem: Some properties may hold by chance in observed executions but not be true invariants.
• Solution: Report confidence levels — how likely is this a true invariant vs. coincidence?
• Heuristics: Properties that hold across diverse inputs are more likely to be true invariants.

Applications

• Program Comprehension: Understand what properties the code maintains.
• Regression Testing: Check that invariants still hold after code changes.
• Bug Finding: Invariant violations indicate bugs.

``python # Detected invariant: balance >= 0 # Test case: withdraw(1000) when balance = 500 # Invariant violated! Bug found: insufficient funds check missing ``

• Formal Verification: Use detected invariants as loop invariants or function contracts for verification tools.
• Test Oracle Generation: Use invariants to check test outputs — if invariant is violated, test failed.

LLM-Based Invariant Detection

• Code Analysis: LLMs analyze code to hypothesize likely invariants without execution.
• Trace Analysis: LLMs analyze execution traces to identify patterns.
• Natural Language: LLMs express invariants in human-readable form.
• Refinement: LLMs refine detected invariants based on developer feedback.

Example: LLM Detecting Invariants

# Code:
def binary_search(arr, target):
    left, right = 0, len(arr) - 1
    while left <= right:
        mid = (left + right) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1

# LLM-detected invariants:
"""
Precondition:
  - arr is sorted in ascending order

Loop invariants:
  - 0 <= left <= len(arr)
  - -1 <= right < len(arr)
  - left <= right + 1
  - If target is in arr, it's in arr[left:right+1]

Postcondition:
  - If target found: 0 <= return < len(arr) and arr[return] == target
  - If target not found: return == -1
"""

Challenges

• False Positives: Properties that hold by chance but aren't true invariants.
• Incomplete Coverage: Only detects invariants evident in observed executions — may miss invariants that require rare inputs.
• Scalability: Analyzing large programs with many variables generates many candidate invariants.
• Noise: Too many reported invariants can overwhelm developers.
• Validation: Determining which detected invariants are meaningful requires human judgment.

Evaluation Metrics

• Precision: What percentage of reported invariants are true?
• Recall: What percentage of actual invariants are detected?
• Usefulness: Do detected invariants help developers understand or verify code?

Tools

• Daikon: The classic invariant detection tool for Java, C, C++.
• Agitator: Commercial tool with invariant detection for Java.
• DySy: Dynamic symbolic execution with invariant inference.

Invariant detection is a powerful program analysis technique — it automatically discovers implicit properties that govern program behavior, providing valuable insights for understanding, testing, and verifying software.