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: http://www.cs.tau.ac.il/~msagiv/

Research interests: static analysis, proof automation,

Contributions

DeepSpec 2018Keynote Speaker of Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems within the DeepSpec 2018-track
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
PLDI 2019Author of Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions within the PLDI Research Papers-track
SPLASH 2018Author of Secure Serverless Computing Using Dynamic Information Flow Control within the Posters-track
Author of Secure Serverless Computing Using Dynamic Information Flow Control within the OOPSLA-track
PLDI 2018Committee Member in External Program Committee
Author of Modularity for Decidability of Deductive Verification with Applications to Distributed Systems within the PLDI Research Papers-track
POPL 2018Author of Reducing Liveness to Safety in First-Order Logic within the Research Papers-track
Author of Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts within the Research Papers-track
Author of Reducing Liveness to Safety in First-Order Logic within the Artifact Evaluation-track
Author of Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts within the Artifact Evaluation-track
RDP 2017Author of Discussion within the RDP-track
Session Chair of Session II (part of RDP)
Author of Welcome within the RDP-track
Organizing Chair in Program Committee within the RDP-track
Session Chair of Welcome (part of RDP)
VMCAI 2017Author of Conjunctive Abstract Interpretation using Paramodulation within the VMCAI-track
Author of Property Directed Reachability for Proving Absence of Concurrent Modification Errors within the VMCAI-track
POPL 2017Committee Member in Program Committee within the POPL-track
SPLASH 2017Author of Paxos Made EPR: Decidable Reasoning about Distributed Protocols within the OOPSLA-track
PLDI 2016Committee Member in External Program Committee
Author of Ivy: Safety Verification by Interactive Generalization within the Research Papers-track
POPL 2016Author of Decidability of Inferring Inductive Invariants within the Research Papers-track
Session Chair of Track 1: Foundations of distributed systems (part of Research Papers)
ESOP 2015Committee Member in Program Committee within the ESOP-track
PLDI 2015Author of Composing Concurrency Control within the Research Papers-track
ECOOP 2015Presenter of Verifying Correctness of Statefull Networks within the Summer School-track
SPLASH 2014Committee Member in External Review Committee within the OOPSLA-track
SPLASH 2013Author of Turning Nondeterminism into Parallelism within the OOPSLA-track
SPLASH 2012Author of Understanding the behavior of database operations under program control within the OOPSLA Research Papers-track