ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mooly Sagiv

Not registered as user yet

Name: Mooly Sagiv

Bio: My research focuses on easing the task of developing reliable and efficient software systems. I am particularly interested in static program analysis which combines two disciplines: automated theorem proving and abstract interpretation. In the next decade, I am hoping to develop useful techniques in order to change the ways modern software is built. I am particularly interested in proof automation, given a program and a requirement, automatically prove or disprove that all executions of the program satisfy the requirements. This problem is in general undecidable and untractable. I am interested in developing practical solutions to proof-automation by: (i) exploring modularity of the system and (ii) relying on semi-automatic and interactive process, where the user manually and interactively guides the proof automation, and (iii) simplifying the verification task by using domain-specific abstractions expressed in a decidable logic. I am applying these techniques to verify safety of liveness of distributed systems.

Country: Israel

Affiliation: Tel Aviv University

Personal website:

Research interests: static analysis, proof automation,


ETAPS 2019Keynote Speaker of From Shape Analysis to Smart Contract Verification: A journey in proof automation within the Mentoring Workshop-track
Author of Automatic Detection of all Smart Contract Bugs within the Mooly Fest-track
Keynote Speaker in Speakers within the Mentoring Workshop-track
Show activities from other conferences

ETAPS 2019-profile
View general profile