| 2018 | ICSOC | 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 |
| 2016 | ICSOC | 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 |
| 2014 | IFM | Verifying Behavioral UML Systems via CEGAR. | Yael Meller, Orna Grumberg, Karen Yorav |
| 2012 | FM | Applying Software Model Checking Techniques for Behavioral UML Models. | Orna Grumberg, Yael Meller, Karen Yorav |
| 2012 | FMCAD | Complete and effective robustness checking by means of interpolation. | Stefan Frehse, Grschwin Fey, Eli Arbel, Karen Yorav, Rolf Drechsler |
| 2009 | FMCAD | SAT-based synthesis of clock gating functions using 3-valued abstraction. | Eli Arbel, Oleg Rokhlenko, Karen Yorav |
| 2009 | FMCAD | Scalable conditional equivalence checking: An automated invariant-generation based approach. | Jason Baumgartner, Hari Mony, Michael L. Case, Jun Sawada, Karen Yorav |
| 2008 | CAV | Functional Verification of Power Gated Designs by Compositional Reasoning. | Cindy Eisner, Amir Nahir, Karen Yorav |
| 2007 | DAC | On-The-Fly Resolve Trace Minimization. | Ohad Shacham, Karen Yorav |
| 2005 | TACAS | SATABS: SAT-Based Predicate Abstraction for ANSI-C. | Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav |
| 2003 | DAC | Behavioral consistency of C and verilog programs using bounded model checking. | Edmund M. Clarke, Daniel Kroening, Karen Yorav |
| 2003 | ICCD | Specifying and Verifying Systems with Multiple Clocks. | Edmund M. Clarke, Daniel Kroening, Karen Yorav |