Students’ Theses

For my information, please mail to orna ‘at’ if you download a thesis.

Karen Yorav, Ph.D. Thesis, June 2000:
Exploiting Syntactic Structure for Automatic Verification
Sagi Katz, M.Sc. Thesis, December 2001:
Techniques for Increasing Coverage of Formal Verification
Doron Bustan, Ph.d. Thesis, July 2002:
Equivalence-Based Reductions and Checking for Preorders
Sharon Keidar-Barner, M.Sc. Thesis, December 2002:
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking
Sharon Shoham, M.Sc. Thesis, November 2003:
A Game-Based Framework for CTL Counterexamples and Abstraction-Refinement
Tamir Heyman, Ph.d. Thesis, December 2003:
Distributed Symbolic Model Checking
Avi Yadgar, M.Sc. Thesis, March 2004:
Memory Efficient ALL-Solutions SAT solver and its Application for Reachability Analysis
Alon Flaisher, M.Sc. Thesis, August 2004:
Enhanced Vacuity Detection in Linear Temporal Logic
Nili Ifergan, M.Sc. Thesis, July 2005:
Achieving High-Speedups in Distributed Reachability Analysis through Asynchronous Computation
Rachel Tzoref, M.Sc. Thesis, June 2006:
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
Rotem Oshman, M.Sc. Thesis, July 2008:
Bounded Model-Checking for Branching-Time Logic

Sharon Shoham, Ph.d. Thesis, January 2009:
Abstraction-Refinement and Modularity in Mu-Calculus Model Checking
Yael Meller, M.Sc. Thesis, January 2010:
Multi-Valued Abstraction and Compositional Model Checking
Avi Yadgar, Ph.d. Thesis, March 2010:
New Approaches to Model Checking and to 3-Valued Abstraction and Refinement
Yakir Vizel, Ph.d. Thesis, May 2014:
SAT-based Model Checking Using Interpolation and IC3
Yael Meller, Ph.d. Thesis, January 2016:
Model Checking Techniques for Behavioral UML Models
Karam Abd ElKader, M.Sc. Thesis, February 2016:
Automated Circular Assume-Guarantee Reasoning
Adi Sosnovich, Ph.D. Thesis, March 2017:
Finding Security Vulnerabilities in Network Protocols Using Methods of Formal Verification 
Anna Trostanetski, M.Sc. Thesis, November 2017:
Modular demand-Driven Analysis of Semantic Difference for Program Versions
Dan Rasin, M.Sc. Thesis, March 2018:
Modular Verification of Concurrent Programs via Sequential Model

Nurit Devir, M.Sc.Thesis, February 2019:
Applying Machine Learning for Identifying Attacks at Run-Time

Bat-Chen Rothenberg, Ph.D. Thesis, December 2020:
Formal Automated Program Repair

Ohad Goudsmid. M.Sc. Thesis, 2021:
Model-Checking of Multi-Properties

Gal Sade, M.Sc. Thesis, 2021:
On-the-fly Model Checking with Guided Abstraction

Hadar Frenkel, Ph.D. Thesis, July 2021:
Automata over Infinite Data Domains: Learnability and Applications in Program Verification and Repair

Ron Marcovich, M.Sc. Thesis, December 2022:
Protocol Inference from program executable using symbolic execution and automata learning