Shahar Maoz's Homepage

Shahar Maoz is a Professor at the School of Computer Science and AI in Tel Aviv University. He received his PhD from the Weizmann Institute of Science in 2009 and has been at Tel Aviv University since 2012. His research interest is in Software Engineering, specifically software and systems modeling, testing, formal specification languages, and synthesis. His work has been funded by an ERC Starting Grant (2015), an ERC Proof of Concept Grant (2022), an ISF Grant (2023), a BSF Grant (2025), and a DFG-ISF grant (2025). He spent sabbaticals in MIT CSAIL and in King's College London. He served as PC Co-Chair of ASE'22 main research track.

Shahar co-organized the first International SPECS summer school in 2023 (SPECS23@TAU) and the second in 2025 (SPECS25@CMU). He co-organized a Dagstuhl Seminar on Specification Engineering in 2025.

Shahar actively recruits new MSc students, PhD students, and post-docs. Positions come with full funding for a number of years. Please contact him for details.

• DFG-ISF (German – Israel) Grant: SPECENG (10/2025, with Lars Grunske)
• BSF (U.S. – Israel Binational Science Foundation) Grant (10/2025, with Eunsuk Kang)
• ISF (Israel Science Foundation) Grant: SPECTACKLE (10/2023)
• ERC Proof of Concept Grant: SYNTACT (5/2022)
• ERC Starting Grant: SYNTECH (4/2015)
• GIF (German-Israeli Foundation) Grant: C&C Views (started 2015, with Bernhard Rumpe)

• ACM TOSEM 4/26: An Empirical Study on the Impact of Example Traces on LTL Comprehension
• FM'26: Performance Heuristics for GR(1) Unrealizable Core Computation
• SoSyM 2/26: Reactive Synthesis Specification Review for Validity and Quality
• ACM TOSEM 11/25: Leveraging Symmetry in GR(1) Synthesis
• ASE'25: Evolution-Aware Heuristics for GR(1) Realizability Checking
• ACM TOSEM 9/25: Exploring Development Methods for Reactive Synthesis Specifications
• ACM TOSEM 6/25: What Properties Affect Boolean Formula Comprehension in Formal Specifications?
• TACAS'25: Performance Heuristics for GR(1) Realizability Checking and Related Analyses
• ICSE'24: Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) Specifications
• ICSE'23: Using Reactive Synthesis: An End-to-End Exploratory Case Study
• ICSE'23: Triggers for Reactive Synthesis Specifications
• ICSE'23: Which of My Assumptions are Unnecessary for Realizability and Why Should I Care?
• ICSE'23 (NIER): Anti-Patterns (Smells) in Temporal Specifications
• MODELS'22: Validating the Correctness of Reactive Systems Specifications Through Systematic Exploration
• ICSE'22: Dynamic Update for Synthesized GR(1) Controllers
• FM'21: Efficient Algorithms for Omega-Regular Energy Games
• ICSE'21: Unrealizable Cores for Reactive Systems Specifications
• SoSyM: Spectra: A Specification Language for Reactive Systems
• FAOC: GR(1)*: GR(1) Specifications Extended with Existential Guarantees
• ASE'20: Just-In-Time Reactive Synthesis
• ESEC/FSE'20: Inherent Vacuity for GR(1) Specifications
• ASE'19: Size and Accuracy in Model Inference
• ASE'19: Statistical Log Differencing
• FM'19: GR(1)*: GR(1) Specifications Extended with Existential Guarantees
• ICSE'19: Symbolic Repairs for GR(1) Specifications
• ESEC/FSE'18: Using Finite-State Models for Log Differencing
• ESEC/FSE'18: Modify, Enhance, Select: Co-Evolution of Combinatorial Models and Test Plans
• ESEC/FSE'17: A Symbolic Justice Violations Transition System for Unrealizable GR(1) Specifications
• MoDELS'17: Why Is My Component and Connector Views Specification Unsatisfiable?
• MoDELS'17: Component and Connector Views in Practice: An Experience Report
• ICSE'17: Syntactic and Semantic Differencing for Combinatorial Models of Test Designs
• FSE'16: On Well-Separation of GR(1) Specifications
• ASE'16: Visualization of Combinatorial Models and Test Plans
• ICSE'16: Behavioral log analysis with statistical guarantees
• ESEC/FSE'15: GR(1) synthesis for LTL specification patterns
• ESEC/FSE'15, New Ideas Track: Behavioral log analysis with statistical guarantees
• MoDELS'15: A framework for relating semantic and syntactic differences
• ASE'15: Have we seen enough traces?
• ASE'14, New Ideas track (log confidence for k-Tails)
• ICSE'14 (verification of structural component and connector views)
• FASE'14 (semantically configurable analysis of scenario-based specifications)
• ASE'13 (mining branching-time scenarios)
• ESEC/FSE'13 (synthesis of component and connector models from crosscutting structural views)
• ICSE'13 (executing unrealizable scenario-based specifications)

• ASE SC member (since 2022)
• PC co-chair for ASE'21 tools track, PC co-chair for ASE'22 main research track
• PC member for ASE'13, ASE'14, MODELS'14, ICSE'15 (RC), ASE'15 (Distinguished Reviewer Award), MODELS'15, ECOOP'16, ASE'16 (ERP), ME'16, OCL'16, ASE'17, ME'17, ICSE'18, ASE'18, ICSE'19, ICSE'20, ASE'20, ESEC/FSE'21, ICSE'22, FoSSaCS'23, ICSE'23, ICSE'24, FSE'24, ICSE'25, ASE'25, ATVA'25, ICSE'26, FormaliSE'26 (Distinguished Reviewer Award), FSE'26, ASE'26
• Reviewer for ACM TOSEM, IEEE TSE, SoSyM, Empirical Software Engineering, Computing Surveys, JSME, STVR, Software: Practice and Experience