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