| 2024 | ATVA | CTL | Mishel Carelli, Orna Grumberg |
| 2023 | ATVA | Structure-Guided Solution of Constrained Horn Clauses. | Omer Rappoport, Orna Grumberg, Yakir Vizel |
| 2021 | VMCAI | Compositional Model Checking for Multi-properties. | Ohad Goudsmid, Orna Grumberg, Sarai Sheinvald |
| 2020 | CAV | Must Fault Localization for Program Repair. | Bat-Chen Rothenberg, Orna Grumberg |
| 2020 | TACAS | Assume, Guarantee or Repair. | Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald |
| 2018 | ATVA | Modular Verification of Concurrent Programs via Sequential Model Checking. | Dan Rasin, Orna Grumberg, Sharon Shoham |
| 2018 | ICSE | Program repair that learns from mistakes. | Bat-Chen Rothenberg, Orna Grumberg |
| 2017 | SAS | Modular Demand-Driven Analysis of Semantic Difference for Program Versions. | Anna Trostanetski, Orna Grumberg, Daniel Kroening |
| 2016 | CAV | Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. | Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham |
| 2016 | FM | Sound and Complete Mutation-Based Program Repair. | Bat-Chen Rothenberg, Orna Grumberg |
| 2015 | FM | Automated Circular Assume-Guarantee Reasoning. | Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham |
| 2015 | LPAR | Analyzing Internet Routing Security Using Model Checking. | Adi Sosnovich, Orna Grumberg, Gabi Nakibly |
| 2014 | ATVA | A Game-Theoretic Approach to Simulation of Data-Parameterized Systems. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2014 | IFM | Verifying Behavioral UML Systems via CEGAR. | Yael Meller, Orna Grumberg, Karen Yorav |
| 2013 | ATVA | An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2013 | CAV | Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems. | Adi Sosnovich, Orna Grumberg, Gabi Nakibly |
| 2013 | TACAS | Intertwined Forward-Backward Reachability Analysis Using Interpolants. | Yakir Vizel, Orna Grumberg, Sharon Shoham |
| 2012 | ATVA | Model Checking Systems and Specifications with Parameterized Atomic Propositions. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2012 | FM | Applying Software Model Checking Techniques for Behavioral UML Models. | Orna Grumberg, Yael Meller, Karen Yorav |
| 2012 | FMCAD | Lazy abstraction and SAT-based reachability in hardware model checking. | Yakir Vizel, Orna Grumberg, Sharon Shoham |
| 2010 | LATA | Variable Automata over Infinite Alphabets. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2009 | ATVA | 3-Valued Abstraction for (Bounded) Model Checking. | Orna Grumberg |
| 2009 | ATVA | A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. | Yael Meller, Orna Grumberg, Sharon Shoham |
| 2009 | FMCAD | Interpolation-sequence based model checking. | Yakir Vizel, Orna Grumberg |
| 2008 | CAV | Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. | Himanshu Jain, Edmund M. Clarke, Orna Grumberg |
| 2008 | TACAS | Efficient Automatic STE Refinement Using Responsibility. | Hana Chockler, Orna Grumberg, Avi Yadgar |
| 2007 | ATVA | 3-Valued Circuit SAT for STE with Automatic Refinement. | Orna Grumberg, Assaf Schuster, Avi Yadgar |
| 2007 | ATVA | A New Approach to Bounded Model Checking for Branching Time Logics. | Rotem Oshman, Orna Grumberg |
| 2007 | SAS | Compositional Verification and 3-Valued Abstractions Join Forces. | Sharon Shoham, Orna Grumberg |
| 2006 | CAV | Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. | Rachel Tzoref, Orna Grumberg |
| 2006 | LICS | 3-Valued Abstraction: More Precision at Less Cost. | Sharon Shoham, Orna Grumberg |
| 2005 | ATVA | Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. | Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster |
| 2005 | ATVA | Multi-valued Model Checking Games. | Sharon Shoham, Orna Grumberg |
| 2005 | CAV | Bounded Model Checking of Concurrent Programs. | Ishai Rabinovitz, Orna Grumberg |
| 2005 | IFM | State/Event Software Verification for Branching-Time Specifications. | Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Jol Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith |
| 2005 | POPL | Proof-guided underapproximation-widening for multi-process systems. | Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald |
| 2005 | VMCAI | Untitled record | Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham |
| 2004 | FMCAD | Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. | Orna Grumberg, Assaf Schuster, Avi Yadgar |
| 2004 | TACAS | Monotonic Abstraction-Refinement for CTL. | Sharon Shoham, Orna Grumberg |
| 2003 | CAV | Enhanced Vacuity Detection in Linear Temporal Logic. | Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi |
| 2003 | CAV | Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. | Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang |
| 2003 | CAV | A Work-Efficient Distributed Algorithm for Reachability Analysis. | Orna Grumberg, Tamir Heyman, Assaf Schuster |
| 2003 | CAV | A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. | Sharon Shoham, Orna Grumberg |
| 2003 | MEMOCODE | High Level Verification of Control Intensive Systems Using Predicate Abstraction. | Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang |
| 2002 | CAV | Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. | Sharon Barner, Orna Grumberg |
| 2002 | IFM | A Framework for Translating Models and Specifications. | Shmuel Katz, Orna Grumberg |
| 2002 | IFM | Translations between Textual Transition Systems and Petri Nets. | Katerina Korenblat, Orna Grumberg, Shmuel Katz |
| 2002 | TACAS | Applicability of Fair Simulation. | Doron Bustan, Orna Grumberg |
| 2001 | CAV | Distributed Symbolic Model Checking for µ-Calculus. | Orna Grumberg, Tamir Heyman, Assaf Schuster |
| 2000 | CADE | Simulation Based Minimization. | Doron Bustan, Orna Grumberg |
| 2000 | CAV | Counterexample-Guided Abstraction Refinement. | Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith |
| 2000 | CAV | Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. | Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster |
| 2000 | FMCAD | Scalable Distributed On-the-Fly Symbolic Model Checking. | Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster |
| 1998 | TACAS | Modular Model Checking of Software. | Karen Laster, Orna Grumberg |
| 1996 | CAV | Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. | Srgio Vale Aguiar Campos, Orna Grumberg |
| 1995 | CONCUR | Veryfying Parameterized Networks using Abstraction and Regular Languages. | Edmund M. Clarke, Orna Grumberg, Somesh Jha |
| 1995 | DAC | Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. | Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao |
| 1995 | LICS | Efficient On-the-Fly Model Checking for CTL* | Girish Bhat, Rance Cleaveland, Orna Grumberg |
| 1994 | CAV | Another Look at LTL Model Checking. | Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi |
| 1993 | CAV | Generation of Reduced Models for Checking Fragments of CTL. | Dennis Dams, Orna Grumberg, Rob Gerth |
| 1993 | CONCUR | Branching Time Temporal Logic and Amorphous Tree Automata. | Orna Bernholtz, Orna Grumberg |
| 1992 | CAV | Modular Abstractions for Verifying Real-Time Distributed Systems. | Hana De-Leon, Orna Grumberg |
| 1992 | ICALP | Program Composition via Unification. | Limor Fix, Nissim Francez, Orna Grumberg |
| 1992 | POPL | Model Checking and Abstraction. | Edmund M. Clarke, Orna Grumberg, David E. Long |
| 1991 | CONCUR | Model Checking and Modular Verification. | Orna Grumberg, David E. Long |
| 1991 | ICALP | Program Composition and Modular Verification. | Limor Fix, Nissim Francez, Orna Grumberg |
| 1990 | CAV | The Modular Framework of Computer-Aided Verification. | Gil Shurek, Orna Grumberg |
| 1990 | POPL | Fairness and Hyperfairness in Multi-Party Interactions. | Paul C. Attie, Nissim Francez, Orna Grumberg |
| 1987 | PODC | Avoiding The State Explosion Problem in Temporal Logic Model Checking. | Edmund M. Clarke, Orna Grumberg |
| 1986 | PODC | Reasoning About Networks With Many Identical Finite-State Processes. | Edmund M. Clarke, Orna Grumberg, Michael C. Browne |
| 1984 | PODC | Fail Termination of Communicating Processe. | Orna Grumberg, Nissim Francez, Shmuel Katz |