Publications




Refereed Conferences

SAT-based synthesis of clock gating functions using 3-valued abstraction
Eli Arbel, Oleg Rokhlenko, and Karen Yorav
In Proc. 9th International Conference on Formal Methods in Computer Aided Design (FMCAD'09), November 2009.

Scalable Conditional Equivalence Checking: An Automated Invariant-Generation Based Approach
Jason Baumgartner Hari Mony Michael Case Jun Sawada Karen Yorav
In Proc. 9th International Conference on Formal Methods in Computer Aided Design (FMCAD'09), November 2009.

Functional Verification of Power Gated Designs by Compositional Reasoning
Cindy Eisner, Amir Nahir, and Karen Yorav
In Proc. 20th International Conference on Computer Aided Verification (CAV'08), July 2008.

On-The-Fly Resolve Trace Minimization
Ohad Shacham and Karen Yorav
In Proc. 44th Design Automation Conference (DAC'07), June 2007.

SATABS: SAT-based predicate abstraction for ANSI-C
Edmund M. Clarke, Daniel Kroening, Natasha Sharygina and Karen Yorav
In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05). Springer, LNCS 3440, April 2005.

Specifying and verifying systems with multiple clocks
Edmund M. Clarke, Daniel Kroening and Karen Yorav
In Proc. International Conference on Computer Design (ICCD'03). October 2003.

Behavioral consistency of C and Verilog programs using bounded model checking
Edmund M. Clarke, Daniel Kroening and Karen Yorav
In Proc. 40th Design Automation Conference (DAC'03). June 2003.

Reproducing synchronization bugs with model checking
Karen Yorav, Sagi Katz and Ron Kiper
In Proc. 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01). Springer, LNCS 2144, September 2001.

First-Order-CTL Model Checking
Jurgen Bohn, Werner Damm, Orna Grumberg, Hardi Hungar and Karen Yorav
In Foundations of Software Technology and Theoretical Computer Science. Springer, LNCS 1530, December 1998.

Modular model checking of software
Karen Yorav and Orna Grumberg
In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98). Springer, March 1998.




Journals

Assumption based distribution of CTL model checking
Lubos Brim, Jitka Crhova and Karen Yorav
In International Journal of Software Tools for Technology Transfer 7(1), February 2005.

Efficient verification of sequential and concurrent C programs
Sagar Chaki, Edmund M. Clarke, Alex Groce, Joel Ouaknine, Ofer Strichman and Karen Yorav
In Formal Methods in System Design 25(2-3), September 2004.

Predicate abstraction of ANSI-C programs using SAT
Daniel Kroening, Natasha Sharygina and Karen Yorav
In Formal Methods in System Design 25(2-3), September 2004.

Test sequence generation and model checking using dynamic transition relations
Sergio Campos, Orna Grumberg, Karen Yorav and Fady Copty
In Journal of Software Tools for Technology Transfer (STTT) 6(2), August 2004.

Static analysis for state-space reductions preserving temporal logics
Karen Yorav and Orna Grumberg
In Formal Methods in System Design 25(1), July 2004.

Syntax-directed model checking of sequential programs
Karen Yorav and Orna Grumberg
In Journal of Logic and Algebraic Programming 52(1), August 2002.

Content navigation