PhD and MSc Theses

PhD and MSc Theses, since 1988

Advisor PROFESSOR EMERITUS Orna Grumberg
Advisor's Email orna@cs.technion.ac.il
Advisor's Home-Site http://www.cs.technion.ac.il/~orna
No of theses 35
Department Computer Science
Department Web Site www.cs.technion.ac.il
Student's Name Graduation Year Degree Abstracts Research Name
Rothenberg Bat-Chen 2021 PhD Abstracts Formal Automated Program Repair
Frenkel Hadar 2021 PhD Abstracts Automata over Infinite Data Domains:Learnability and Applications in Program Verification and Repair
Sosnovich Adi 2017 PhD Abstracts Finding Security Vulnerabilities in Network Protocols Using Methods of Formal Verification
Meller Yael 2016 PhD Abstracts Model Checking Techniques for Behavioral UML Models
Vizel Yakir 2014 PhD Abstracts SAT-Based Model Checking Using Interpolation and IC3
Yadgar Avraham 2010 PhD Abstracts New Approaches to Model Checking and to 3-Valued Abstraction and Refinement
Shoham Buchbinder Sharon 2009 PhD Abstracts Abstraction-Refinement and Modularity in Mu-Calculus Model Checking
Bustan Doron 2002 PhD Abstracts Equivalence-Based Reductions and Checking for Preorders
Kupferman-Bernholtz Orna 1995 PhD Model Checking for Branching-Time Temporal Logics
Heyman Tamir 2004 PhD Abstracts Distributed Symbolic Model Checking
Yorav Karen 2000 PhD Exploiting Syntactic Structure for Automatic Verification
Marcovich Ron 2023 MSc Abstracts Protocol Inference from Program Executable using Symbolic Execution and Automata Learning
Goudsmid Ohad 2021 MSc Abstracts Compositional Model-Checking of Multi-Properties
Sade Gal 2021 MSc Abstracts On-the-Fly Model Checking with Guided Abstraction
Devir Nurit 2019 MSc Abstracts Applying Machine Learning for Identifying Attacks at Run-Time
Rasin Dan 2018 MSc Abstracts Modular Verification of Concurrent Programs via Sequential Model Checking
Trostanetski Anna 2018 MSc Abstracts Modular Demand-Driven Analysis of Semantic Difference for Program Versions
Abdelkader Karam 2016 MSc Abstracts Automated Circular Assume-Guarantee Reasoning
Flur Shaked 2013 MSc Abstracts Weak Omega Automata
Meller Yael 2010 MSc Abstracts Multi Valued Abstraction and Compositional Model Checking
Oshman Rotem 2008 MSc Abstracts Bounded Model – Checking for Branching-Time Logic
Brel Rachel 2006 MSc Abstracts Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
Ifergan Nili 2005 MSc Abstracts Achieving High Speedups in Distributed Reachability Analysis through Asynchronous Computation
Yadgar Avraham 2004 MSc Abstracts Solving All-SAT Problem for Reachability Analysis
Shoham Buchbinder Sharon 2004 MSc Abstracts A Game-Based Framework for CTL Counterexamples and Abstraction-Refinement
Keidar Sharon 2003 MSc Abstracts Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking
Katz Sagi 2002 MSc Techniques for Increasing Coverage of Formal Verification
Livne Shlomo 2001 MSc Machine Learning for Efficient BDD Variable Ordering in Verification
Rinetskey Noam 2001 MSc Interprocedural Shape Analysis
Gershon Benjamin 1994 MSc Synthesis of Concurrent Systems
De-Lion Hana 1991 MSc Real Time Temporal Logics
Marelly Rami 1991 MSc Automatic Verifier of Distributed Algorithms
Shurek Gil 1991 MSc Modular Computer Aided Verification of Concurrent Systems
Shtapler Zeiev 1990 MSc Automatic Verification of Distributed Algorithms
Leyzerovitch Esther 1989 MSc Impiementing Superimpositions for Occam