A Compete Proof Rule for Strong Equifair Termination. - Orna Grumberg; Nissim Francez; Shmuel Katz (Logic of Programs, 1983)

Fail Termination of Communicating Processe. - Orna Grumberg; Nissim Francez; Shmuel Katz (PODC, 1984)

Proving Termination of Prolog Programs. - Nissim Francez; Orna Grumberg; Shmuel Katz; Amir Pnueli (Logic of Programs, 1985)

A Proof Rule for Fair Termination of Guarded Commands - Orna Grumberg; Nissim Francez; Johann A. Makowsky; Willem P. de Roever (Inf. Control., 1985)

A Complete Rule for Equifair Termination. - Orna Grumberg; Nissim Francez; Shmuel Katz (J. Comput. Syst. Sci., 1986)

Avoiding The State Explosion Problem in Temporal Logic Model Checking. - Edmund M. Clarke; Orna Grumberg (PODC, 1987)

Characterizing Kripke Structures in Temporal Logic. - Michael C. Browne; Edmund M. Clarke; Orna Grumberg (TAPSOFT, Vol.1, 1987)

The Model Checking Problem for Concurrent Systems with Many Similar Processes. - Edmund M. Clarke; Orna Grumberg (Temporal Logic in Specification, 1987)

Characterizing Finite Kripke Structures in Propositional Temporal Logic. - Michael C. Browne; Edmund M. Clarke; Orna Grumberg (Theor. Comput. Sci., 1988)

Infinite Trees, Markings and Well-Foundedness - Ran Rinat; Nissim Francez; Orna Grumberg (Inf. Comput., 1988)

Network Grammars, Communication Behaviors and Automatic Verification. - Ze'ev Shtadler; Orna Grumberg (Automatic Verification Methods for Finite State Systems, 1989)

Reasoning about Networks with Many Identical Finite State Processes - Michael C. Browne; Edmund M. Clarke; Orna Grumberg (Inf. Comput., 1989)

The Modular Framework of Computer-Aided Verification. - Gil Shurek; Orna Grumberg (CAV, 1990)

Sematics-Driven Decompositions for the Verification of Distributed Programs. - Limor Fix; Nissim Francez; Orna Grumberg (Programming Concepts and Methods, 1990)

Program Composition and Modular Verification. - Limor Fix; Nissim Francez; Orna Grumberg (ICALP, 1991)

A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. - Edmund M. Clarke; Orna Grumberg; Robert P. Kurshan (J. Log. Comput., 1992)

Generation of Reduced Models for Checking Fragments of CTL. - Dennis Dams; Orna Grumberg; Rob Gerth (CAV, 1993)

Branching Time Temporal Logic and Amorphous Tree Automata. - Orna Bernholtz; Orna Grumberg (CONCUR, 1993)

Verification Tools for Finite-State Concurrent Systems. - Edmund M. Clarke; Orna Grumberg; David E. Long (REX School/Symposium, 1993)

Fairness and Hyperfairness in Multi-Party Interactions. - Paul C. Attie; Nissim Francez; Orna Grumberg (Distributed Comput., 1993)

Modular Abstractions for Verifying Real-Time Distributed Systems. - Hana De-Leon; Orna Grumberg (Formal Methods Syst. Des., 1993)

How Linear Can Branching-Time Be? - Orna Grumberg; Robert P. Kurshan (ICTL, 1994)

Program Composition via Unification. - Limor Fix; Nissim Francez; Orna Grumberg (Theor. Comput. Sci., 1994)

Model Checking and Abstraction. - Edmund M. Clarke; Orna Grumberg; David E. Long (ACM Trans. Program. Lang. Syst., 1994)

Model Checking and Modular Verification. - Orna Grumberg; David E. Long (ACM Trans. Program. Lang. Syst., 1994)

What if model checking must be truly symbolic. - Hardi Hungar; Orna Grumberg; Werner Damm (CHARME, 1995)

Veryfying Parameterized Networks using Abstraction and Regular Languages. - Edmund M. Clarke; Orna Grumberg; Somesh Jha (CONCUR, 1995)

Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. - Edmund M. Clarke; Orna Grumberg; Kenneth L. McMillan; Xudong Zhao 005 (DAC, 1995)

Efficient On-the-Fly Model Checking for CTL* - Girish Bhat; Rance Cleaveland; Orna Grumberg (LICS, 1995)

Verification of the Futurebus+ Cache Coherence Protocol. - Edmund M. Clarke; Orna Grumberg; Hiromi Hiraishi; Somesh Jha; David E. Long; Kenneth L. McMillan; Linda A. Ness (Formal Methods Syst. Des., 1995)

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. - Sérgio Vale Aguiar Campos; Orna Grumberg (CAV, 1996)

Model checking. - Edmund M. Clarke; Orna Grumberg; David E. Long (NATO ASI DPD, 1996)

Branching-Time Temporal Logic and Tree Automata. - Orna Kupferman; Orna Grumberg (Inf. Comput., 1996)

Verification of Temporal Properties. - Limor Fix; Orna Grumberg (J. Log. Comput., 1996)

Buy One, Get One Free!!! - Orna Kupferman; Orna Grumberg (J. Log. Comput., 1996)

Another Look at LTL Model Checking. - Edmund M. Clarke; Orna Grumberg; Kiyoharu Hamaguchi (Formal Methods Syst. Des., 1997)

Verifying Parameterized Networks. - Edmund M. Clarke; Orna Grumberg; Somesh Jha (ACM Trans. Program. Lang. Syst., 1997)

Abstract Interpretation of Reactive Systems. - Dennis Dams; Rob Gerth; Orna Grumberg (ACM Trans. Program. Lang. Syst., 1997)

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)

"Have I written enough Properties?" - A Method of Comparison between Specification and Implementation. - Sagi Katz; Orna Grumberg; Daniel Geist (CHARME, 1999)

Preface. - Alessandro Cimatti; Orna Grumberg (SMC@FLoC, 1999)

State Space Reduction Using Partial Order Techniques. - Edmund M. Clarke; Orna Grumberg; Marius Minea; Doron A. Peled (Int. J. Softw. Tools Technol. Transf., 1999)

Simulation Based Minimization. - Doron Bustan; Orna Grumberg (CADE, 2000)

Counterexample-Guided Abstraction Refinement. - Edmund M. Clarke; Orna Grumberg; Somesh Jha; Yuan Lu 004; Helmut Veith (CAV, 2000)

Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. - Tamir Heyman; Daniel Geist; Orna Grumberg; Assaf Schuster (CAV, 2000)

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. - Sérgio Vale Aguiar Campos; Edmund M. Clarke; Orna Grumberg (Formal Methods Syst. Des., 2000)

Model checking, 1st Edition. - Edmund M. Clarke; Orna Grumberg; Doron A. Peled (MIT Press, 2001)

Progress on the State Explosion Problem in Model Checking. - Edmund M. Clarke; Orna Grumberg; Somesh Jha; Yuan Lu 004; Helmut Veith (Informatics, 2001)

Introduction: Special Issue on CAV '97. - Orna Grumberg (Formal Methods Syst. Des., 2001)

Which Branching-Time Properties are Effectively Linear? - Orna Grumberg; Robert P. Kurshan (J. Log. Comput., 2001)

A Framework for Translating Models and Specifications. - Shmuel Katz; Orna Grumberg (IFM, 2002)

Translations between Textual Transition Systems and Petri Nets. - Katerina Korenblat; Orna Grumberg; Shmuel Katz (IFM, 2002)

Preface. - Lubos Brim; Orna Grumberg (PDMC@CONCUR, 2002)

Different directions in parallel and distributed model checking (invited talk). - Orna Grumberg (PDMC@CONCUR, 2002)

A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits. - Tamir Heyman; Daniel Geist; Orna Grumberg; Assaf Schuster (Formal Methods Syst. Des., 2002)

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

Enhanced Vacuity Detection in Linear Temporal Logic. - Roy Armoni; Limor Fix; Alon Flaisher; Orna Grumberg; Nir Piterman; Andreas Tiemeyer; Moshe Y. Vardi (CAV, 2003)

Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. - Edmund M. Clarke; Orna Grumberg; Muralidhar Talupur; Dong Wang (CAV, 2003)

High Level Verification of Control Intensive Systems Using Predicate Abstraction. - Edmund M. Clarke; Orna Grumberg; Muralidhar Talupur; Dong Wang (MEMOCODE, 2003)

Counterexample-guided abstraction refinement for symbolic model checking. - Edmund M. Clarke; Orna Grumberg; Somesh Jha; Yuan Lu 004; Helmut Veith (J. ACM, 2003)

Learning to Order BDD Variables in Verification. - Orna Grumberg; Shlomi Livne; Shaul Markovitch (J. Artif. Intell. Res., 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)

Simulation-based minimazation. - Doron Bustan; Orna Grumberg (ACM Trans. Comput. Log., 2003)

Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. - Orna Grumberg; Assaf Schuster; Avi Yadgar (FMCAD, 2004)

Monotonic Abstraction-Refinement for CTL. - Sharon Shoham; Orna Grumberg (TACAS, 2004)

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

Applicability of fair simulation. - Doron Bustan; Orna Grumberg (Inf. Comput., 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)

Bounded Model Checking of Concurrent Programs. - Ishai Rabinovitz; Orna Grumberg (CAV, 2005)

Regular Vacuity. - Doron Bustan; Alon Flaisher; Orna Grumberg; Orna Kupferman; Moshe Y. Vardi (CHARME, 2005)

Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. - Orna Grumberg; Tamir Heyman; Nili Ifergan; Assaf Schuster (CHARME, 2005)

Abstraction and Refinement in Model Checking. - Orna Grumberg (FMCO, 2005)

State/Event Software Verification for Branching-Time Specifications. - Sagar Chaki; Edmund M. Clarke; Orna Grumberg; Joël Ouaknine; Natasha Sharygina; Tayssir Touili; Helmut Veith (IFM, 2005)

Proof-guided underapproximation-widening for multi-process systems. - Orna Grumberg; Flavio Lerda; Ofer Strichman; Michael Theobald (POPL, 2005)

Don't Know in the µ-Calculus. - Orna Grumberg; Martin Lange; Martin Leucker; Sharon Shoham (VMCAI, 2005)

Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. - Sharon Barner; Orna Grumberg (Formal Methods Syst. Des., 2005)

Distributed Symbolic Model Checking for µ-Calculus. - Orna Grumberg; Tamir Heyman; Assaf Schuster (Formal Methods Syst. Des., 2005)

Introductory paper. - Lubos Brim; Orna Grumberg (Int. J. Softw. Tools Technol. Transf., 2005)

Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. - Rachel Tzoref; Orna Grumberg (CAV, 2006)

A work-efficient distributed algorithm for reachability analysis. - Orna Grumberg; Tamir Heyman; Assaf Schuster (Formal Methods Syst. Des., 2006)

3-Valued Circuit SAT for STE with Automatic Refinement. - Orna Grumberg; Assaf Schuster; Avi Yadgar (ATVA, 2007)

A New Approach to Bounded Model Checking for Branching Time Logics. - Rotem Oshman; Orna Grumberg (ATVA, 2007)

When not losing is better than winning: Abstraction and refinement for the full mu-calculus. - Orna Grumberg; Martin Lange; Martin Leucker; Sharon Shoham (Inf. Comput., 2007)

Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. - Limor Fix; Orna Grumberg; Amnon Heyman; Tamir Heyman; Assaf Schuster (Int. J. Found. Comput. Sci., 2007)

VeriTech: a framework for translating among model description notations. - Orna Grumberg; Shmuel Katz (Int. J. Softw. Tools Technol. Transf., 2007)

A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. - Sharon Shoham; Orna Grumberg (ACM Trans. Comput. Log., 2007)

Efficient Automatic STE Refinement Using Responsibility. - Hana Chockler; Orna Grumberg; Avi Yadgar (TACAS, 2008)

3-Valued abstraction: More precision at less cost. - Sharon Shoham; Orna Grumberg (Inf. Comput., 2008)

3-Valued Abstraction for (Bounded) Model Checking. - Orna Grumberg (ATVA, 2009)

Hybrid BDD and All-SAT Method for Model Checking. - Avi Yadgar; Orna Grumberg; Assaf Schuster (Languages: From Formal to Natural, 2009)

Interpolation-sequence based model checking. - Yakir Vizel; Orna Grumberg (FMCAD, 2009)

The 2008 CAV Award citation. - Randal E. Bryant; Orna Grumberg; Thomas A. Henzinger; Moshe Y. Vardi (Formal Methods Syst. Des., 2009)

Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. - Himanshu Jain; Edmund M. Clarke; Orna Grumberg (Formal Methods Syst. Des., 2009)

Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification. - Michael Huth 001; Orna Grumberg (Int. J. Softw. Tools Technol. Transf., 2009)

Variable Automata over Infinite Alphabets. - Orna Grumberg; Orna Kupferman; Sarai Sheinvald (LATA, 2010)

2009 CAV award announcement. - Randal E. Bryant; Orna Grumberg; Joseph Sifakis; Moshe Y. Vardi (Formal Methods Syst. Des., 2010)

Compositional verification and 3-valued abstractions join forces. - Sharon Shoham; Orna Grumberg (Inf. Comput., 2010)

2-Valued and 3-Valued Abstraction-Refinement in Model Checking. - Orna Grumberg (Logics and Languages for Reliability and Security, 2010)

Model Checking Systems and Specifications with Parameterized Atomic Propositions. - Orna Grumberg; Orna Kupferman; Sarai Sheinvald (ATVA, 2012)

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

Lazy abstraction and SAT-based reachability in hardware model checking. - Yakir Vizel; Orna Grumberg; Sharon Shoham (FMCAD, 2012)

2010 CAV award announcement. - Orna Grumberg; Moshe Y. Vardi; Joseph Sifakis; Rajeev Alur (Formal Methods Syst. Des., 2012)

Multi-valued model checking games. - Sharon Shoham; Orna Grumberg (J. Comput. Syst. Sci., 2012)

Model Checking: From BDDs to Interpolation. - Orna Grumberg (Software Safety and Security, 2012)

An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. - Orna Grumberg; Orna Kupferman; Sarai Sheinvald (ATVA, 2013)

Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems. - Adi Sosnovich; Orna Grumberg; Gabi Nakibly (CAV, 2013)

Intertwined Forward-Backward Reachability Analysis Using Interpolants. - Yakir Vizel; Orna Grumberg; Sharon Shoham (TACAS, 2013)

A Game-Theoretic Approach to Simulation of Data-Parameterized Systems. - Orna Grumberg; Orna Kupferman; Sarai Sheinvald (ATVA, 2014)

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

SAT-based Model Checking: Interpolation, IC3, and Beyond. - Orna Grumberg; Sharon Shoham; Yakir Vizel (Software Systems Safety, 2014)

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

Analyzing Internet Routing Security Using Model Checking. - Adi Sosnovich; Orna Grumberg; Gabi Nakibly (LPAR, 2015)

Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. - Karam Abd Elkader; Orna Grumberg; Corina S. Pasareanu; Sharon Shoham (CAV (1), 2016)

Sound and Complete Mutation-Based Program Repair. - Bat-Chen Rothenberg; Orna Grumberg (FM, 2016)

Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201). - Julian Dolby; Orna Grumberg; Peter Müller 001; Omer Tripp (Dagstuhl Reports, 2016)

A framework for compositional verification of multi-valued systems via abstraction-refinement. - Yael Meller; Orna Grumberg; Sharon Shoham (Inf. Comput., 2016)

Learning-Based Compositional Model Checking of Behavioral UML Systems. - Orna Grumberg; Yael Meller (Dependable Software Systems Engineering, 2016)

An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data. - Hadar Frenkel; Orna Grumberg; Sarai Sheinvald (NFM, 2017)

Modular Demand-Driven Analysis of Semantic Difference for Program Versions. - Anna Trostanetski; Orna Grumberg; Daniel Kroening (SAS, 2017)

Formal Black-Box Analysis of Routing Protocol Implementations. - Adi Sosnovich; Orna Grumberg; Gabi Nakibly (CoRR, 2017)

Model checking, 2nd Edition. - Edmund M. Clarke; Orna Grumberg; Daniel Kroening; Doron A. Peled; Helmut Veith (MIT Press, 2018)

Modular Verification of Concurrent Programs via Sequential Model Checking. - Dan Rasin; Orna Grumberg; Sharon Shoham (ATVA, 2018)

Program repair that learns from mistakes. - Bat-Chen Rothenberg; Orna Grumberg (ICSE (Companion Volume), 2018)

Automated circular assume-guarantee reasoning. - Karam Abd Elkader; Orna Grumberg; Corina S. Pasareanu; Sharon Shoham (Formal Aspects Comput., 2018)

Abstraction and Abstraction Refinement. - Dennis Dams; Orna Grumberg (Handbook of Model Checking, 2018)

Topology-Agnostic Runtime Detection of OSPF Routing Attacks. - Nurit Devir; Orna Grumberg; Shaul Markovitch; Gabi Nakibly (CNS, 2019)

An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains. - Hadar Frenkel; Orna Grumberg; Sarai Sheinvald (J. Autom. Reason., 2019)

Must Fault Localization for Program Repair. - Bat-Chen Rothenberg; Orna Grumberg (CAV (2), 2020)

Assume, Guarantee or Repair. - Hadar Frenkel; Orna Grumberg; Corina S. Pasareanu; Sarai Sheinvald (TACAS (1), 2020)

Compositional Model Checking for Multi-properties. - Ohad Goudsmid; Orna Grumberg; Sarai Sheinvald (VMCAI, 2021)

Automated Program Repair Using Formal Verification Techniques. - Hadar Frenkel; Orna Grumberg; Bat-Chen Rothenberg; Sarai Sheinvald (Principles of Systems Design, 2022)

Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties (full version). - Hadar Frenkel; Orna Grumberg; Corina S. Pasareanu; Sarai Sheinvald (CoRR, 2022)

Edmund Melson Clarke, Jr. (1945-2020). - Sicun Gao; Orna Grumberg; Paolo Zuliani (Formal Methods Syst. Des., 2022)

Assume, guarantee or repair: a regular framework for non regular properties. - Hadar Frenkel; Orna Grumberg; Corina S. Pasareanu; Sarai Sheinvald (Int. J. Softw. Tools Technol. Transf., 2022)

Structure-Guided Solution of Constrained Horn Clauses. - Omer Rappoport; Orna Grumberg; Yakir Vizel (ATVA, 2023)

Condition Synthesis Realizability via Constrained Horn Clauses. - Bat-Chen Rothenberg; Orna Grumberg; Yakir Vizel; Eytan Singher (NFM, 2023)

CTL* Verification and Synthesis Using Existential Horn Clauses. - Mishel Carelli; Orna Grumberg (ATVA (2), 2024)

CTL* Verification and Synthesis using Existential Horn Clauses. - Mishel Carelli; Orna Grumberg (CoRR, 2024)