We envision a future where
safety-critical
cyber-physical
AI-integrated systems
operate under rigorous mathematical safety proofs.
-
Grounded in theory
Provable safety built on foundational principles -
Machine-checked proofs
Absolute logical correctness through mechanical validation.
Research Digest
Formal Theory of
Real-Time Systems
We establish mathematical foundations and mechanized proofs to guarantee that timing-critical systems always meet their deadlines with absolute certainty.
Scalable Verification of Complex Systems
We develop scalable verification methodologies to manage exponential complexity, ensuring that rigorous formalization remains feasible for large-scale, real-world infrastructures.
AI meets
Formal Verification
We explore the synergy between AI and formal methods, providing rigorous safety guarantees for AI and leveraging AI to automate complex formal proofs.
Join Us
Welcome Aboard VeSL!
We are recruiting!
We welcome prospective PhD students, master's students, and undergraduate researchers.
Don’t hesitate to reach out — if you enjoy precise thinking, logic, proofs, or trustworthy systems, we would love to hear from you.
Contact: send an email to me!
Recent News
Verified Systems Lab Is Now Open
The Verified Systems Laboratory in the Department of Electrical Engineering and Computer Science at DGIST officially opened on November 1st, 2025.