VERIFICATION
& VALIDATION
TECHNIQUES
LECTURE NOTES
Università degli Studi di Udine · A.A. 2025–2026
Personal lecture notes developed from the Verification and Validation Techniques lectures, with interactive companions.
Covers finite-state automata, NFA-to-DFA subset construction, ε-closure and ε-removal, product automata, and reachability fixpoint algorithms, as well as formal verification concepts like LTL and Model Checking. Major theorems have guided Proof Labs, and the complete lecture notes remain available as a downloadable PDF.
Course Materials
PROOF LABS
Interactive Theorem Proofs
Predict each proof step, inspect the dominant visual, and reveal the formal justification
NOTEBOOKS
Interactive Notebooks
26 browser-based notebooks, grouped by chapter — from DFAs and subset construction to Büchi automata, ω-regular complementation, LTL, and model checking
MAPS
Interactive Chapter Mind Maps
Explore all 15 chapters from their main arteries down to individual topics
PDF
Full Lecture Notes
Download or read the complete lecture notes PDF
Verification & Validation
UniUD
Runs completely in-browser via Pyodide