Methodology and System for Practical Formal Verification of Reactive Hardware. - Ilan Beer; Shoham Ben-David; Daniel Geist; Raanan Gewirtzman; Michael Yoeli (CAV, 1994)

RuleBase: An Industry-Oriented Formal Verification Tool. - Ilan Beer; Shoham Ben-David; Cindy Eisner; Avner Landver (DAC, 1996)

RuleBase: Model Checking at IBM. - Ilan Beer; Shoham Ben-David; Cindy Eisner; Daniel Geist; Leonid Gluhovsky; Tamir Heyman; Avner Landver; P. Paanah; Yoav Rodeh; G. Ronin; Yaron Wolfsthal (CAV, 1997)

Efficient Detection of Vacuity in ACTL Formulaas. - Ilan Beer; Shoham Ben-David; Cindy Eisner; Yoav Rodeh (CAV, 1997)

On-the-Fly Model Checking of RCTL Formulas. - Ilan Beer; Shoham Ben-David; Avner Landver (CAV, 1998)

The Temporal Logic Sugar. - Ilan Beer; Shoham Ben-David; Cindy Eisner; Dana Fisman; Anna Gringauze; Yoav Rodeh (CAV, 2001)

Efficient Detection of Vacuity in Temporal Model Checking. - Ilan Beer; Shoham Ben-David; Cindy Eisner; Yoav Rodeh (Formal Methods Syst. Des., 2001)

PathFinder: A Tool for Design Exploration. - Shoham Ben-David; Anna Gringauze; Baruch Sterin; Yaron Wolfsthal (CAV, 2002)

An Algorithmic Approach to Design Exploration. - Sharon Barner; Shoham Ben-David; Anna Gringauze; Baruch Sterin; Yaron Wolfsthal (FME, 2002)

Model Checking at IBM. - Shoham Ben-David; Cindy Eisner; Daniel Geist; Yaron Wolfsthal (Formal Methods Syst. Des., 2003)

Scalable distributed on-the-fly symbolic model checking. - Shoham Ben-David; Orna Grumberg; Tamir Heyman; Assaf Schuster (Int. J. Softw. Tools Technol. Transf., 2003)

The Safety Simple Subset. - Shoham Ben-David; Dana Fisman; Sitvanit Ruah (Haifa Verification Conference, 2005)

Model checking the basic modalities of CTL with Description Logic. - Shoham Ben-David; Richard J. Trefler; Grant E. Weddell (Description Logics, 2006)

Temporal Antecedent Failure: Refining Vacuity. - Shoham Ben-David; Dana Fisman; Sitvanit Ruah (CONCUR, 2007)

Modal vs. Propositional Reasoning for model checking with Description Logics. - Shoham Ben-David; Richard J. Trefler; Grant E. Weddell (Description Logics, 2007)

Bounded Model Checking with Description Logic Reasoning. - Shoham Ben-David; Richard J. Trefler; Grant E. Weddell (TABLEAUX, 2007)

Embedding finite automata within regular expressions. - Shoham Ben-David; Dana Fisman; Sitvanit Ruah (Theor. Comput. Sci., 2008)

Fair Cycle Detection using Description Logic Reasoning. - Shoham Ben-David; Jeffrey Pound; Richard J. Trefler; Dmitry Tsarkov; Grant E. Weddell (Description Logics, 2009)

Applications of Description Logic and Causality in Model Checking. - Shoham Ben-David (2009)

Monitoring and Recovery of Web Service Applications. - Jocelyn Simmonds; Shoham Ben-David; Marsha Chechik (The Smart Internet, 2010)

Guided recovery for web service applications. - Jocelyn Simmonds; Shoham Ben-David; Marsha Chechik (SIGSOFT FSE, 2010)

Optimizing Computation of Recovery Plans for BPEL Applications - Jocelyn Simmonds; Shoham Ben-David; Marsha Chechik (TAV-WEB, 2010)

Model Checking Using Description Logic. - Shoham Ben-David; Richard J. Trefler; Grant E. Weddell (J. Log. Comput., 2010)

Partial models: a position paper. - Michalis Famelis; Shoham Ben-David; Marsha Chechik; Rick Salay (MoDeVVa@MoDELS, 2011)

CSSL: a logic for specifying conditional scenarios. - Shoham Ben-David; Marsha Chechik; Arie Gurfinkel; Sebastián Uchitel (SIGSOFT FSE, 2011)

Explaining counterexamples using causality. - Ilan Beer; Shoham Ben-David; Hana Chockler; Avigail Orni; Richard J. Trefler (Formal Methods Syst. Des., 2012)

A Framework for Ranking Vacuity Results. - Shoham Ben-David; Orna Kupferman (ATVA, 2013)

Merging Partial Behaviour Models with Different Vocabularies. - Shoham Ben-David; Marsha Chechik; Sebastián Uchitel (CONCUR, 2013)

Attention-Based Coverage Metrics. - Shoham Ben-David; Hana Chockler; Orna Kupferman (Haifa Verification Conference, 2013)

Monitoring and recovery for web service applications. - Jocelyn Simmonds; Shoham Ben-David; Marsha Chechik (Computing, 2013)

Supporting incremental behaviour model elaboration. - Sebastián Uchitel; Dalal Alrajeh; Shoham Ben-David; Víctor A. Braberman; Marsha Chechik; Guido de Caso; Nicolás D'Ippolito; Dario Fischbein; Diego Garbervetsky; Jeff Kramer; Alessandra Russo; German E. Sibay (Comput. Sci. Res. Dev., 2013)

Symbolic Model Checking of Product-Line Requirements Using SAT-Based Methods. - Shoham Ben-David; Baruch Sterin; Joanne M. Atlee; Sandy Beidu (ICSE (1), 2015)

Modeling Product Lines with Kripke Structures and Modal Logic. - Zinovy Diskin; Aliakbar Safilian; Tom Maibaum; Shoham Ben-David (ICTAC, 2015)

Vacuity in practice: temporal antecedent failure. - Shoham Ben-David; Fady Copty; Dana Fisman; Sitvanit Ruah (Formal Methods Syst. Des., 2015)

Observational Refinement and Merge for Disjunctive MTSs. - Shoham Ben-David; Marsha Chechik; Sebastián Uchitel (ATVA, 2016)

Faithful Modeling of Product Lines with Kripke Structures and Modal Logic. - Zinovy Diskin; Aliakbar Safilian; Tom Maibaum; Shoham Ben-David (Sci. Ann. Comput. Sci., 2016)