Shoham Ben-David

Postdoctoral research in Computer Science
The Hebrew University of Jerusalem
Research Topics: 
1. Merge of Partial Behavior Models. 2. Probability of Temporal Logic Formulas.

Shoham Ben-David completed her PhD at the University of Waterloo in Canada, and in 2011 undertook her postdoctoral research as an Azrieli Fellow at the Hebrew University's School of Computer Science. Her research focused on formal methods for hardware and software programs. Her goal was to define a new partial formalism which would allow software components to be designed separately, and then composed automatically, into one functioning program.
 
Currently she is working as a postdoctoral researcher in the University of Waterloo, with Professor Jo Atlee, as part of the NECIS research partnership.
 
A personal perspective:
In Shoham's words: " I very much enjoyed my period as an Azrieli Fellow. From an academic point of view, I was lucky to have the opportunity to work with a first-rate researcher who is well known and appreciated worldwide.
The volunteer work that I did as an Azrieli Fellow, teaching Mathematics to young people, was a remarkable experience in itself which I plan to return to in the future.
But this is only the beginning. When I think of the period I spent as an Azrieli Fellow, two prominent key aspects arise:
Firstly, the "VIP treatment" I received from the Azrieli Fellows staff, who consistently indulged us with their warmth, personal interest, and dedication to organizing high level events for the Fellows.
The second aspect was the introduction to the other Fellows - a group of such nice, talented people that you usually do not get to meet in your everyday life, but in the Azrieli Fellows' framework we met every few weeks. What is so special about the Azrieli Fellows Program is the exposure to people from a variety of fields – Science, Education, Architecture and more.
Although I have met many people in academic work, the Azrieli Fellows were always people with similar interests, much the same as mine.
All this created a feeling of being part of an elite team with a great, accepting, and warm environment, promoting expanded horizons yet at the same time, not competitive – undoubtedly a once in a lifetime experience!  …"
 
  

Journals:

• Sebastian Uchitel, Dalal Alrajeh, Shoham Ben-David, Victor Braberman,Marsha Chechik, Guido De Caso, Nicolas D’Ippolito, Dario Fischbein, Diego Garbervetsky, Jeff Kramer, Alessandra Russo, German Sibay.  Supporting incremental behaviour model elaboration. Computer Science - Research and Development. Accepted for publication
 
• Jocelyn Simmonds, Shoham Ben-David, Marsha Chechik. 2013. Monitoring and recovery for web service applications. Computing 95(3): 223-267. 

• Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail orni, Richard J. Trefler. 2012. Explaining Counterexamples Using Causality. Formal Methods System Design (FMSD) 40(1): 20-40

Shoham Ben-David, Richard Trefler, Grant Weddell. 2010. Model Checking with Description Logic. Journal of Logic and Computation 20(1): 111-131.

Shoham Ben-David, Dana Fisman, Sitvanit Ruah. 2008. Embedding Finite Automata within Regular Expressions. Theoretical Computer Science 404(3): 202-218.

Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster. 2003. Scalable Distributed On-the-Fly Symbolic Model Checking. International Journal on Software Tools for Technology Transfer 4(4): 496-504.

Shoham Ben-David, Cindy Eisner, Daniel Geist, Yaron Wolfsthal. 2003. Model Checking at IBM. Formal Methods in System Design 22(2): 101-108.

• Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh. 2001. Efficient Detection of Vacuity in Temporal Model Checking. Formal Methods in System Design 18(2): 141-163.


Refereed Conference Papers:

• Shoham Ben-David, Orna Kupferman.  A Framework for Ranking Vacuity Results. Accepted to conference: the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13) 

• Shoham Ben-David, Marsha Chechik, Sebastian Uchitel. Merging Partial Behavior Models with Different Vocabularies. Accepted to conference: the 24th International Conference on Concurrency Theory (CONCUR'13)

Shoham Ben-David, Marsha Chechik, Arie Gurfinkel and Sebasti´an Uchitel. CSSL: A Logic for Specifying Conditional Scenarios. In: Gyimóthy and Zeller Andreas, editors. SIGSOFT FSE. Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of Software engineering; 2011 September 5-9; Szeged, Hungary. ACM;  2011. p. 37-47

• Jocelyn Simmonds, Shoham Ben-David and Marsha Chechik. Guided Recovery for Web Service Applications. In: Roman Gruia-Catalin and Sullivan Kevin J., editors. SIGSOFT FSE. Proceedings of the 18th ACM SIGSOFT symposium on Foundations of software engineering;  2010 November 7-11; Santa Fe, NM, USA. ACM; 2011. p. 247-256

• Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail orni and Richard Trefler. Explaining Counterexamples Using Causality. In: Bouajjani Ahmed and Maler Oded, editors. Computer Aided Verification, 21st International Conference, CAV 2009; 2009 June 26 - July 2; Grenoble, France. Lecture Notes in Computer Science 5643 Springer; 2009. p. 94-108

Shoham Ben-David, Dana Fisman and Sitvanit Ruah. Temporal Antecedent Failure: Refining Vacuity. In: Caires Luís and Thudichum Vasconcelos Vasco, editors. Concurrency Theory, 18th International Conference, CONCUR; 2007 September 3-8; Lisbon, Portugal. Lecture Notes in Computer Science 4703 Springer ; 2007.p. 493-506

Shoham Ben-David, Richard Trefler and Grant Weddell. Bounded Model Checking with Description Logic Reasoning. In: Olivetti Nicola, editor.  Automated Reasoning with Analytic Tableaux and Related Methods, 16th International Conference, TABLEAUX; 2007 July 3-6; Aix en Provence, France. Lecture Notes in Computer Science 4548 Springer; 2007. p. 60-72

Shoham Ben-David, Dana Fisman and Sitvanit Ruah. The Safety Simple Subset. In: Ur Shmuel, Bin Eyal and Wolfsthal Yaron, editors. Hardware and Software Verification and Testing, First International Haifa Verification Conference, Revised Selected Papers; 2005 November 13-16; Haifa, Israel. Lecture Notes in Computer Science 3875 Springer; 2006.p.14-29

Shoham Ben-David, Dana Fisman and Sitvanit Ruah. Embedding Finite Automata within Regular Expressions. In: Margaria Tiziana and Steffen Bernhard, editors.  Revised Selected Papers:  Leveraging Applications of Formal Methods, First International Symposium, ISoLA;  2004 October 30 - November 2; Paphos, Cyprus. Lecture Notes in Computer Science 4313 Springer; 2006. p. 175-180

Shoham Ben-David, Anna Gringauze, Baruch Sterin and Yaron Wolfsthal.  PathFinder: A Tool for Design Exploration. In: Brinksma Ed and Guldstrand Larsen Kim, editors. Computer Aided Verification, 14th International Conference, CAV; 2002 July 27-31; Copenhagen, Denmark. Lecture Notes in Computer Science 2404 Springer; 2002. p. 510-514

• Sharon Barner, Shoham Ben-David, Anna Gringauze, Baruch Sterin and Yaron Wolfsthal. An Algorithmic Approach to Design Exploration. In: Eriksson Lars-Henrik and Lindsay  Peter A., Editors. International Symposium of Formal Methods Europe, FME; 2002 July 22-24; Copenhagen, Denmark. Lecture Notes in Computer Science 2391 Springer; 2002. p. 146-162

• Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze and Yoav Rodeh. The Temporal Logic Sugar. In: Berry Gérard and Alain Finkel Hubert, editors. Computer Aided Verification, 13th International Conference, CAV;  2001 July 18-22; Paris, France. Lecture Notes in Computer Science 2102 Springer; 2001. p. 363-367

Shoham Ben-David, Tamir Heyman, Orna Grumberg and Assaf Schuster. Scalable Distributed On-the-Fly Symbolic Model Checking. In: Hunt Jr Warren A. and Johnson Steven D., editors. Formal Methods in Computer-Aided Design, Third International Conference, FMCAD; 2000 November 1-3; Austin, Texas, USA. Lecture Notes in Computer Science 1954 Springer; 2000. p. 390-404

• Ilan Beer, Shoham Ben-David and Avner Landver. On-the-Fly Model Checking of RCTL Formulas. In: Hu Alan J. and Vardi Moshe Y., editors.   Computer Aided Verification, 10th International Conference, CAV '98 Proceedings; 1998 June 28 - July 2; Vancouver, BC, Canada. Lecture Notes in Computer Science 1427 Springer; 1998. p. 184-194

• Ilan Beer, Shoham Ben-David, Cindy Eisner and Yoav Rodeh. Efficient Detection of Vacuity in ACTL Formulas. In: Grumberg Orna, editor. Computer Aided Verification, 9th International Conference, CAV '97, Proceedings; 1997 22-25; Haifa, Israel. Lecture Notes in Computer Science 1254 Springer; 1997. p. 279-290

• Ilan Beer, Shoham Ben-David, Cindy. Eisner, Daniel  Geist, Leonid Gluhovsky, Tamir Heyman, Avner Landver, Peter Paanah, Yoav Rodeh, Gregory Ronin and Yaron Wolfsthal. RuleBase: Model Checking at IBM. In:   Grumberg Orna, Editor. Computer Aided Verification, 9th International Conference, CAV '97,  Proceedings; 1997 June 22-25; Haifa, Israel. Lecture Notes in Computer Science 1254 Springer; 1997.p. 480-483

•  Ilan Beer, Shoham Ben-David, Cindy Eisner and Avner Landver. An Industry-Oriented Formal Verification Tool. In: Pennino Thomas and Yoffa Ellen J.,editors. Proceedings of the 33st Conference on Design Automation, DAC; 1996 June 3-7; Las Vegas, Nevada, USA. ACM Press; 1996. p. 655-660

• Ilan Beer, Shoham Ben-David, Daniel Geist, Raanan Gewirtzman and Michael Yoeli. Methodology and System for Practical Formal Verification of Reactive Hardware. In: Dill David L., editor. Computer Aided Verification, 6th International Conference, CAV '94,  Proceedings; 1994 June 21-23; Stanford, California, USA. Lecture Notes in Computer Science 818 Springer; 1994. p. 182-193


Patents:

Shoham Ben-David; Generation of Partial Traces in Model Checking. US Patent 7,155,374, issued December 2006.

Shoham Ben-David and Anna Gringauze; Efficient Production of Disjoint Multiple Traces. US Patent 7,146,301, issued December 2006.

• Ilan Beer, Shoham Ben-David, Leonid Gluhovsky, Yossi Malka and Yaron Wolfsthal; Target Design Model Behavior Explorer. U.S Patent 6,691,078, issued February 2004.

Shoham Ben-David, Leonid Gluhovsky; Time-Memory Tradeoff Control in Counterexample Production. U.S Patent 6,665,848, issued December 2003.