fixpoint

Fixpoint theory is the spine of this entire course.
It drives while-loop semantics in the denotational model, the soundness theorems in abstract interpretation, and the chaotic iteration algorithm in the abstract interpreter. The name is not a metaphor — it is the theorem.

Comprehensive coursework for Software Verification (A.Y. 2025/26), taught by prof. Francesco Ranzato. Covers the full arc from structural operational semantics to a working abstract interpreter, with formal proofs and a software artifact that can be run and extended.

---

Repository structure

fixpoint/
├── semantics/              Operational and Denotational Semantics
│   ├── solutions.tex       LaTeX source — all 12 exercises
│   └── solutions.pdf       Compiled PDF
│
├── static-analysis/        Static Program Analysis — Homework A
│   ├── homework_solutions.tex    LaTeX source — all 12 exercises
│   └── homework_solutions.pdf    Compiled PDF
│
└── whyle/                  Abstract Interpreter — Homework B
    ├── README.md           Whyle-specific documentation
    ├── main.py             CLI entry point
    ├── lang/               Parser and AST for the While language
    ├── cfg/                CFG construction (Miné Fig. 3.9)
    ├── domains/            Abstract domain interface + Int_{m,n}
    ├── semantics/          Transfer functions (E#, C#, S#)
    ├── solver/             Chaotic fixpoint iteration with widening/narrowing
    └── examples/           Sample While programs with expected invariants

---

Part 1 — Operational and Denotational Semantics

Source: semantics/

Twelve exercises covering the standard structural operational semantics (SOS) and denotational semantics of the While language.

Operational Semantics (Exercises 1–6)

#	Statement	Verdict
1	while b do S₁ ∼ while b do (if b then S₁ else S₂)	True
2	repeat S until b ∼ (repeat S until b); (while ¬b do S)	True
3	while b do ((while b do S); S) ∼ (while b do S); S	False — counterexample at x=0
4	S₁ ∼ S₂ ⟹ while b do S₁ ∼ while b do S₂	Proved
5	Composition Lemma: ⟨S₁,s⟩ ⇒ᵏ s′ ⟹ ⟨S₁;S₂,s⟩ ⇒ᵏ ⟨S₂,s′⟩	Proved
6	While⁻ (no assignments) preserves the state	Proved

Denotational Semantics (Exercises 7–12)

#	Statement	Verdict
7	W ∼ W ; W	True — because W(s′)=s′ when W terminates at s′
8	W ∼ if b then (repeat S until ¬b) else skip	True — FIX coincidence
9	W ∼ while b do (S; if b then S else skip)	True — mutual fixpoint argument
10	Define lvar(S) and prove state-preservation outside assigned vars	Proved
11	FIX(f ∘ g) = f(FIX(g ∘ f))	Proved
12	(a) union of convex sets need not be convex; (b) ⟨conv(D),⊆⟩ is a CPO	(a) False, (b) True

---

Part 2 — Static Program Analysis (Homework A)

Source: static-analysis/

Twelve exercises on the mathematical foundations of abstract interpretation and their application to program analysis.

Galois Connections (Exercises 1–4)

#	Topic
1	GC properties: γ(α(⊤))=⊤, α(⊥)=⊥, `α(c) = ⋀{a
2	Characterisation via closure operator: monotone + extensive + idempotent
3	Characterisation via Moore-family closure: ⋀Y ∈ γ(α(C)) for all Y ⊆ γ(α(C))
4	GC pairs (pre_R, post̃_R) and (post_R, prẽ_R) on ℘(S)

Abstract Operations (Exercises 5–8)

#	Topic
5	Equivalence between abstract soundness and concrete over-approximation
6	α-completeness ⟹ α(lfp(f)) = lfp(f♯); counterexample for lfp(f) = γ(lfp(f♯))
7	·ᴵⁿᵗ is α-complete; +ᴵⁿᵗ is α-complete but not exact on non-convex sets
8	·ᶜᵒⁿˢᵗ and +ᶜᵒⁿˢᵗ are both α-complete in the constant domain

Program Analysis (Exercises 9–12)

#	Topic
9	Transfer functions B♯⟦x<k⟧, B♯⟦x>y⟧, A♯⟦x*x⟧, A♯⟦x+y⟧ for the Sign_k domain
10	Program requiring 3-step strictly ascending chain in the Congruence domain
11	Program where the reduced product Karr × Octagon strictly dominates both components
12	Two Interproc/Octagon programs: one yielding the optimal invariant, one not

---

Part 3 — Abstract Interpreter: Whyle (Homework B)

Source: whyle/

A complete, runnable abstract interpreter for the While language, instantiated with the parametric interval domain Int_{m,n}.

Quick start

pip install lark
python whyle/main.py whyle/examples/countdown.while

── Invariants at each program point ──────────────────────────────
  ℓ  2: {x ∈ 0}          [EXIT]
  ℓ  4: {x ∈ [0, 10]}    [LOOP-HEAD]
  ℓ  5: {x ∈ [1, 10]}
  ℓ  6: {x ∈ [0, 9]}

Exit invariant: {x ∈ 0}

Domain modes

Parameters	Domain	Notes
m = −∞, n = +∞	Standard intervals Int	Widening required
m, n ∈ ℤ, m ≤ n	Bounded intervals (finite lattice)	Widening auto-disabled
m > n	Constant propagation	Widening auto-disabled

Key CLI options

# Bounded domain — no widening needed
python whyle/main.py prog.while -m 0 -n 100

# Threshold widening inferred from program constants
python whyle/main.py prog.while --auto-thresholds

# Manual thresholds
python whyle/main.py prog.while --thresholds="-1,0,1,10,11"

# Constrain initial state
python whyle/main.py prog.while --init x=0:50 --init y=0:50

# Inspect the CFG
python whyle/main.py prog.while --show-cfg

See whyle/README.md for the full interface and design rationale.

Theory implemented

Component	Reference
CFG construction	Miné, Fig. 3.9
Abstract equation system AIA(P, s♯)	Miné, §3.5.3, eq. 3.4
Widening ▽	Miné, eq. 4.7
Threshold widening ▽_T	Miné, eq. 4.13
Narrowing △	Miné, eq. 4.10–4.11
Backward condition filtering C♯⟦c⟧	Miné, §4.1.4
Domain Int_{m,n}	Miné, §4.7

---

References

• Miné, A. (2017). Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation. Foundations and Trends in Programming Languages, 4(3–4), 120–372.
• Nielson, F., Nielson, H. R., & Hankin, C. (1999). Principles of Program Analysis. Springer.
• Cousot, P., & Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL '77.
• Ranzato, F. (2025/26). Software Verification — Course slides, University of Padova.

---

Course info

Course	Software Verification
Instructor	Prof. Francesco Ranzato
A.Y.	2025/26
Topics	Operational semantics · Denotational semantics · Abstract interpretation