Theoretical Points 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 total absence

• Formal verification uses mathematical proofs for all valid inputs

What is the Curry-Howard Isomorphism (Propositions-as-Types)?

-Proposition = Type (theorem as type)

• Proof = Program/Value/Term (inhabitant of type)

• Proof verification = Type checking (t : τ matches P ⊢ A)

What does the Type Inhabitation Problem translate to?

-Finding automated proof for theorem A = searching for program t satisfying type signature τ

• Proving t : τ is the verification goal

• Links proof search to program synthesis

What is the decidability trade-off in type systems?

-Weak systems (Simply Typed Lambda Calculus): fully decidable but lack recursion, induction, data structures

• Rich systems (Calculus of Inductive Constructions): sacrifice automatic general decidability

• Gain ability to express complex software safety properties

What is the Simply Typed Lambda Calculus?

-Provided computation without paradoxes

• Term and type inference fully decidable (computer could write proofs automatically)

• Too weak to prove programs correct (lacked polymorphism, recursion, data types)

What is the Calculus of Inductive Constructions (CIC)?

-Rich type system with dependent, inductive, and higher-order types (1988)

• Used by modern provers (Coq/Rocq)

• Scales to verify real-world software while expressing advanced mathematics

What is the De Bruijn Criterion?

-Proof assistant's security relies on small, isolated, trusted kernel type-checker

• Entire mathematical model depends only on this kernel

• Complex automation routines (tactics) are untrusted (outside boundary)

What are the three layers of prover architecture?

-Untrusted UI Layer (user tactics: induction, simpl, destruct)

• Elaboration Layer (assembles detailed λ-calculus terms)

• Isolated Trusted Core Kernel (stripped-down type-checker enforcing soundness)

How does kernel validation work?

-User tactics gradually construct complete lambda-calculus proof term

• Upon Qed, raw proof term passed to kernel

• Tiny type-checker analyzes term from first principles; rejects ill-typed terms

What happens with a buggy tactic execution?

-Tactic script fails to resolve goal or breaks

• No complete proof term sent to type-checker
• System remains sound; theorem simply remains unproven

What happens with a flaw inside the core kernel?

-Soundness bug compromises internal type-checker

• Tool incorrectly evaluates contradictory proof term as valid
• Triggers Principle of Explosion (Ex Falso Quodlibet): any arbitrary proposition becomes provable

What is the well-founded termination constraint in provers?

-All recursive processes must execute across well-founded relation

• Example: structural induction over finite data types
• Prevents infinite loops (would make type-checking undecidable, stalling compiler)

What is Code Extraction?

-Developer specifies and proves core algorithm within prover's type theory

• Prover compiles validated logic into OCaml, Haskell, or Scheme
• Trust shifts to prover's translation algorithm and target compiler

What is Semantic Embedding?

-Write software in standard languages (C, Java) directly

• Embed operational semantics of target language into proof engine
• Verify statements against embedded models sequentially

What is the trust boundary for Semantic Embedding?

-Safety depends on precision of embedded formal framework

• Requires absolute certainty that formalized models map exactly to real-world hardware executions
• Different from code extraction's trust in translation algorithm

What is the B-Method?

-Jean-Raymond Abrial's design framework for correct-by-construction systems

• Uses upfront mathematical refinement pipeline (abstract model → concrete software via step-by-step proofs)
• Example: Paris Metro Line 14 automated safety controls (no runtime verification passes needed)

What is JVM bytecode verification?

-Automated static analysis pass at class-loading time

• Checks raw instruction streams from untrusted remote .class files
• Guarantees type safety, operand stack neutrality (prevents overflows/underflows), and access control

What are the three core safety properties enforced by JVM verification?

-Type safety invariance: every instruction receives operands of exact expected type

• Operand stack neutrality: stack height consistent across all control flow branches, no underflow/overflow
• Access control & memory integrity: private variables protected, reference semantics enforced

What are the two approaches for JVM safety?

-Defensive static runtime pass (standard JVM): data-flow analysis at class-loading time

• Formal ITP modeling: executable interpreter inside proof assistant (Rocq/Coq)
• Correct-by-construction (B-Method): eliminate runtime validation entirely

How are structural properties proved for JVM instructions in ITP?

-Write and prove absolute theorems about entire instruction sets

• Example for IADD (integer add): ∀ s: JVMState, well_formed s → well_formed (exec_instr IADD s)
• Proves valid starting state never causes underflow, type corruption, or stack crash

Why was type theory introduced?

-To avoid paradoxes like Russell's Paradox R = {x | x ∉ x} (1901)

• Russell introduced Type Theory in 1913 requiring objects assigned specific types
• Untyped lambda calculus (1936) was prone to paradoxes (term x x) and non-termination

What is the problem of 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 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 are the three limitations of standard Hoare logic?

-Pointer aliasing problem: two pointers can point to same address, assignment to *p corrupts property about *q

• Shared-memory concurrency explosion: requires analyzing every thread interleaving (combinatorial explosion)
• Cyber-physical continuous divide: cannot model hybrid systems (discrete controller + 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; Guarantee (G): state mutations thread is allowed to cause

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; ⟨α⟩φ: exists path through α terminating in φ

What is Stepwise Refinement/Refinement Calculus?

-Correct-by-construction programming model

• Start with highly abstract, non-executable mathematical specification
• Each refinement step mathematically preserves correctness of preceding model (final code guaranteed correct)