Prof. Doron Peled
Proof of correctness of hardware systems and software Automatic proof, tests of logic systems and formal languages
CV
Professor Peled completed his PhD at the Technion and a postdoctoral fellowship at the University of Warwick. He spent nearly a decade at AT&T Bell Labs and served as a professor at the University of Texas at Austin and the University of Warwick. In 2006, he joined the Bar-Ilan faculty and later served as Head of the Computer Science Department. In 2014, he received the prestigious CAV Award for developing Partial Order Reduction—a technology that enables the highly efficient verification of complex concurrent systems. He is the author of two foundational textbooks, Model Checking and Software Reliability Methods, used by researchers worldwide.
Research
Formal Methods, Software Reliability, and AI
In safety-critical systems, spacecraft navigation, or banking networks, even a minor "bug" can have devastating consequences. The challenge is that modern software is so complex that it is impossible to verify every scenario-the number of system states that require testing exceeds the number of atoms in the universe. Consequently, manual or random testing is insufficient, leaving a constant risk that a critical scenario has been overlooked. Professor Doron Peled develops mathematical methods that prove a system will behave correctly under all possible circumstances- moving beyond "we didn't find a bug" to a definitive mathematical proof that no bug exists. These principles are now applied to verifying code generated by AI tools.
Core Research Areas:
Formal Methods: Mathematical proofs for software and hardware correctness.
Model Checking: Algorithms for the efficient scanning of all system scenarios.
Runtime Verification: Real-time monitoring of system integrity.
AI & LLM Reliability: Monitoring and oversight mechanisms for AI-generated code.
Research Character:
Theoretical-Applied: Developing rigorous mathematical proofs alongside functional tools used in industry and agencies such as NASA.
Career Horizons:
Lab graduates integrate into diverse roles:
Industry: Software Reliability Engineers and verification experts for mission-critical systems (Aviation, Medical, Autonomous Vehicles).
Academia: Researchers and lecturers in formal methods and software security.
High-Tech: Developers of AI-generated code verification tools at leading tech companies.
Last Updated Date : 30/07/2026
