Methods and techniques for program verification 2

What is the fundamental limitation of dynamic testing?

-Executes program on finite subset of inputs to locate flaws

• Can prove presence of bugs but cannot guarantee absence

• Formal verification uses mathematical proofs for all valid inputs

What is a Hoare Triple?

-{P} S {Q} where P = precondition (before statement)

• S = program statement/loop/block
• Q = postcondition (must hold after execution if P satisfied)

What is the problem with manual assertions in Hoare logic?

-Requires humans to guess intermediate assertions to bridge gaps between statements

• Highly non-deterministic verification process
• Uses inference rules (Assignment, Composition, Conditionals) but needs manual guidance

What is Dijkstra's Weakest Precondition (wp)?

-Complete, deterministic strategy working backward through program structure

• wp(S,Q) computes weakest, least-restrictive predicate P that must hold before S to guarantee termination and Q
• Automates deductive verification

What are the Guarded Command Language rules for wp?

-Assignment: wp(x:=E, Q) = Q[x→E] (substitute E for x in Q)

• Composition: wp(S1;S2, Q) = wp(S1, wp(S2, Q))
• Maps code statements to primitive relational commands

What is the Verification Condition (VC)?

-After wp(S,Q) calculated, compiler checks if declared precondition P implies wp(S,Q) (P ⇒ wp(S,Q))

• Implication handed to automated SMT Solver (e.g., Z3 behind Dafny)
• Automatically checks if code matches contracts

What is the Pointer Aliasing Problem?

-Standard Hoare logic assumes changing one variable doesn't affect others

• In C/Java, two pointers can point to same address (aliasing)
• Assignment to *p can corrupt property proved about *q, invalidating proof deductions

What is the Shared-Memory Concurrency Explosion?

-Multiple processes read/write same memory simultaneously

• Threads can interleave arbitrarily
• Requires analyzing every possible thread interleaving → combinatorial state-space explosion

What is the Cyber-Physical Continuous Divide?

-Standard Hoare logic operates on discrete state steps only

• Cannot model hybrid systems (autonomous vehicles, medical implants)
• Hybrid systems couple discrete software controller with continuous physics governed by differential equations

What is Separation Logic?

-Solved: pointer aliasing and mutable heap allocation problem

• Splits memory into independent spatial sections
• Separating Conjunction (P * Q): P and Q hold in disjoint, non-overlapping memory regions

What is Rely/Guarantee Reasoning?

-Solved: state-space explosion of shared-memory concurrent systems

• Each thread verified in isolation against environmental contract
• Rely (R): interference thread can tolerate from environment; Guarantee (G): state mutations thread is allowed to cause

What is the Rely/Guarantee composition rule?

-Concurrent execution proven safe if each thread's Guarantee satisfies Rely conditions of all neighboring threads

• Verified in isolation (no need to track all interleavings)
• Component specified by two distinct assertions

What is Dynamic Logic?

-Solved: verification for cyber-physical, continuous, and hybrid systems

• Embeds programs directly inside modal logic operators
• [α]φ: after all possible executions of α, φ must hold; ⟨α⟩φ: there exists path through α terminating in φ

What are Probabilistic Predicate Transformers?

-Solved: validation of stochastic, randomized, non-deterministic systems

• Standard logic binary (true/false) insufficient for probability distributions
• Replaces boolean predicates with quantitative functions to compute precise lower/upper bounds of success

What is Stepwise Refinement/Refinement Calculus?

-Solved: difficulty of verifying completed program after the fact

• Correct-by-construction programming model (start with abstract mathematical specification)
• Apply strict mathematical rules step-by-step; each refinement step preserves correctness of preceding model

What is the benefit of correct-by-construction?

-Final generated code guaranteed correct (no subsequent verification passes needed)

• Each individual refinement step mathematically preserves correctness
• Avoids verifying completed program after it's written