First-Order-CTL Model Checking. - Jürgen Bohn 002; Werner Damm; Orna Grumberg; Hardi Hungar; Karen Laster (FSTTCS, 1998)

Modular Model Checking of Software. - Karen Laster; Orna Grumberg (TACAS, 1998)

Exploiting syntactic structure for automatic verification. - Karen Yorav (2000)

Reproducing Synchronization Bugs with Model Checking. - Karen Yorav; Sagi Katz; Ron Kiper (CHARME, 2001)

Using Assumptions to Distribute CTL Model Checking. - Lubos Brim; Jitka Crhová; Karen Yorav (PDMC@CONCUR, 2002)

Syntax-directed model checking of sequential programs. - Karen Yorav; Orna Grumberg (J. Log. Algebraic Methods Program., 2002)

Behavioral consistency of C and verilog programs using bounded model checking. - Edmund M. Clarke; Daniel Kroening; Karen Yorav (DAC, 2003)

Specifying and Verifying Systems with Multiple Clocks. - Edmund M. Clarke; Daniel Kroening; Karen Yorav (ICCD, 2003)

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. - Sagar Chaki; Joël Ouaknine; Karen Yorav; Edmund M. Clarke (SoftMC@CAV, 2003)

Efficient Verification of Sequential and Concurrent C Programs. - Sagar Chaki; Edmund M. Clarke; Alex Groce; Joël Ouaknine; Ofer Strichman; Karen Yorav (Formal Methods Syst. Des., 2004)

Predicate Abstraction of ANSI-C Programs Using SAT. - Edmund M. Clarke; Daniel Kroening; Natasha Sharygina; Karen Yorav (Formal Methods Syst. Des., 2004)

Static Analysis for State-Space Reductions Preserving Temporal Logics. - Karen Yorav; Orna Grumberg (Formal Methods Syst. Des., 2004)

Test sequence generation and model checking using dynamic transition relations. - Sérgio Vale Aguiar Campos; Orna Grumberg; Karen Yorav; Fady Copty (Int. J. Softw. Tools Technol. Transf., 2004)

SATABS: SAT-Based Predicate Abstraction for ANSI-C. - Edmund M. Clarke; Daniel Kroening; Natasha Sharygina; Karen Yorav (TACAS, 2005)

Adaptive Application of SAT Solving Techniques. - Ohad Shacham; Karen Yorav (BMC@CAV, 2005)

Assumption-based distribution of CTL model checking. - Lubos Brim; Karen Yorav; Jitka Zidkova (Int. J. Softw. Tools Technol. Transf., 2005)

On-The-Fly Resolve Trace Minimization. - Ohad Shacham; Karen Yorav (DAC, 2007)

Functional Verification of Power Gated Designs by Compositional Reasoning. - Cindy Eisner; Amir Nahir; Karen Yorav (CAV, 2008)

SAT-based synthesis of clock gating functions using 3-valued abstraction. - Eli Arbel; Oleg Rokhlenko; Karen Yorav (FMCAD, 2009)

Scalable conditional equivalence checking: An automated invariant-generation based approach. - Jason Baumgartner; Hari Mony; Michael L. Case; Jun Sawada; Karen Yorav (FMCAD, 2009)

Haifa verification conference 2007. - Karen Yorav (Int. J. Softw. Tools Technol. Transf., 2009)

Preface. - Armin Biere; Karen Yorav (Formal Methods Syst. Des., 2011)

Applying Software Model Checking Techniques for Behavioral UML Models. - Orna Grumberg; Yael Meller; Karen Yorav (FM, 2012)

Complete and effective robustness checking by means of interpolation. - Stefan Frehse; Görschwin Fey; Eli Arbel; Karen Yorav; Rolf Drechsler (FMCAD, 2012)

Verifying Behavioral UML Systems via CEGAR. - Yael Meller; Orna Grumberg; Karen Yorav (IFM, 2014)

Learning-Based Compositional Model Checking of Behavioral UML Systems. - Yael Meller; Orna Grumberg; Karen Yorav (FACS, 2015)

COOL: A Model-Driven and Automated System for Guided and Verifiable Cloud Solution Design. - Hamid R. Motahari Nezhad; Karen Yorav; Peifeng Yin; Taiga Nakamura; Scott Trent; Gil Shurek; Takayuki Kushida; Uma Subramanian (ICSOC Workshops, 2016)

A Model-Driven Framework for Automated Generation and Verification of Cloud Solutions from Requirements. - Hamid R. Motahari Nezhad; Taiga Nakamura; Adi Sosnovich; Peifeng Yin; Karen Yorav (ICSOC, 2018)