Orna Grumberg

Yakir Vizel, Orna Grumberg, Sharon Shoham: Intertwined Forward-Backward Reachability Analysis Using Interpolants. TACAS 2013: 308-323

Orna Grumberg, Moshe Y. Vardi, Joseph Sifakis, Rajeev Alur: 2010 CAV award announcement. Formal Methods in System Design 40(2): 117-120 (2012)

Sharon Shoham, Orna Grumberg: Multi-valued model checking games. J. Comput. Syst. Sci. 78(2): 414-429 (2012)

Orna Grumberg, Orna Kupferman, Sarai Sheinvald: Model Checking Systems and Specifications with Parameterized Atomic Propositions. ATVA 2012: 122-136

Orna Grumberg, Yael Meller, Karen Yorav: Applying Software Model Checking Techniques for Behavioral UML Models. FM 2012: 277-292

Yakir Vizel, Orna Grumberg, Sharon Shoham: Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD 2012: 173-181

Orna Grumberg, Shlomi Livne, Shaul Markovitch: Learning to Order BDD Variables in Verification. CoRR abs/1107.0020 (2011)

Javier Esparza, Bernd Spanfelner, Orna Grumberg (Eds.): Logics and Languages for Reliability and Security. NATO Science for Peace and Security Series - D: Information and Communication Security 25, IOS Press 2010, isbn 978-1-60750-099-5

Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi: 2009 CAV award announcement. Formal Methods in System Design 36(3): 195-197 (2010)

Sharon Shoham, Orna Grumberg: Compositional verification and 3-valued abstractions join forces. Inf. Comput. 208(2): 178-202 (2010)

Orna Grumberg, Orna Kupferman, Sarai Sheinvald: Variable Automata over Infinite Alphabets. LATA 2010: 561-572

Orna Grumberg: 2-Valued and 3-Valued Abstraction-Refinement in Model Checking. Logics and Languages for Reliability and Security 2010: 105-128

Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi: The 2008 CAV Award citation. Formal Methods in System Design 35(1): 4-5 (2009)

Himanshu Jain, Edmund M. Clarke, Orna Grumberg: Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Formal Methods in System Design 35(1): 6-39 (2009)

Michael Huth, Orna Grumberg: Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification. STTT 11(2): 85-94 (2009)

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

Yael Meller, Orna Grumberg, Sharon Shoham: A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. ATVA 2009: 271-288

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

Yakir Vizel, Orna Grumberg: Interpolation-sequence based model checking. FMCAD 2009: 1-8

Orna Grumberg, Michael Kaminski, Shmuel Katz, Shuly Wintner (Eds.): Languages: From Formal to Natural, Essays Dedicated to Nissim Francez on the Occasion of His 65th Birthday. Lecture Notes in Computer Science 5533, Springer 2009, isbn 978-3-642-01747-6

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

Himanshu Jain, Edmund M. Clarke, Orna Grumberg: Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. CAV 2008: 254-267

Hana Chockler, Orna Grumberg, Avi Yadgar: Efficient Automatic STE Refinement Using Responsibility. TACAS 2008: 233-248

Orna Grumberg, Helmut Veith (Eds.): 25 Years of Model Checking - History, Achievements, Perspectives. Lecture Notes in Computer Science 5000, Springer 2008, isbn 978-3-540-69849-4

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

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

Orna Grumberg, Shmuel Katz: VeriTech: a framework for translating among model description notations. STTT 9(2): 119-132 (2007)

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

Rotem Oshman, Orna Grumberg: A New Approach to Bounded Model Checking for Branching Time Logics. ATVA 2007: 410-424

Orna Grumberg, Assaf Schuster, Avi Yadgar: 3-Valued Circuit SAT for STE with Automatic Refinement. ATVA 2007: 457-473

Sharon Shoham, Orna Grumberg: Compositional Verification and 3-Valued Abstractions Join Forces. SAS 2007: 69-86

Orna Grumberg, Michael Huth (Eds.): Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. Lecture Notes in Computer Science 4424, Springer 2007, isbn 978-3-540-71208-4

Orna Grumberg, Tamir Heyman, Assaf Schuster: A work-efficient distributed algorithm for reachability analysis. Formal Methods in System Design 29(2): 157-175 (2006)

Rachel Tzoref, Orna Grumberg: Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. CAV 2006: 190-204

Sharon Shoham, Orna Grumberg: 3-Valued Abstraction: More Precision at Less Cost. LICS 2006: 399-410

Orna Grumberg, Tamir Heyman, Assaf Schuster: Distributed Symbolic Model Checking for µ-Calculus. Formal Methods in System Design 26(2): 197-219 (2005)

Sharon Barner, Orna Grumberg: Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. Formal Methods in System Design 27(1-2): 29-66 (2005)

Lubos Brim, Orna Grumberg: Introductory paper. STTT 7(1): 1-3 (2005)

Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster: Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. ATVA 2005: 11-25

Sharon Shoham, Orna Grumberg: Multi-valued Model Checking Games. ATVA 2005: 354-369

Ishai Rabinovitz, Orna Grumberg: Bounded Model Checking of Concurrent Programs. CAV 2005: 82-97

Orna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster: Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. CHARME 2005: 129-145

Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi: Regular Vacuity. CHARME 2005: 191-206

Orna Grumberg: Abstraction and Refinement in Model Checking. FMCO 2005: 219-242

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

Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald: Proof-guided underapproximation-widening for multi-process systems. POPL 2005: 122-131

Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham: Don't Know in the µ-Calculus. VMCAI 2005: 233-249

Karen Yorav, Orna Grumberg: Static Analysis for State-Space Reductions Preserving Temporal Logics. Formal Methods in System Design 25(1): 67-96 (2004)

Doron Bustan, Orna Grumberg: Applicability of fair simulation. Inf. Comput. 194(1): 1-18 (2004)

Sérgio Vale Aguiar Campos, Orna Grumberg, Karen Yorav, Copty Fady: Test sequence generation and model checking using dynamic transition relations. STTT 6(2): 174-182 (2004)

Orna Grumberg, Assaf Schuster, Avi Yadgar: Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. FMCAD 2004: 275-289

Sharon Shoham, Orna Grumberg: Monotonic Abstraction-Refinement for CTL. TACAS 2004: 546-560

Lubos Brim, Orna Grumberg: Preface. Electr. Notes Theor. Comput. Sci. 89(1): 1-2 (2003)

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5): 752-794 (2003)

Orna Grumberg, Shlomi Livne, Shaul Markovitch: Learning to Order BDD Variables in Verification. J. Artif. Intell. Res. (JAIR) 18: 83-116 (2003)

Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster: Scalable distributed on-the-fly symbolic model checking. STTT 4(4): 496-504 (2003)

Doron Bustan, Orna Grumberg: Simulation-based minimazation. ACM Trans. Comput. Log. 4(2): 181-206 (2003)

Orna Grumberg, Tamir Heyman, Assaf Schuster: A Work-Efficient Distributed Algorithm for Reachability Analysis. CAV 2003: 54-66

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

Sharon Shoham, Orna Grumberg: A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. CAV 2003: 275-287

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

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

Lubos Brim, Orna Grumberg: Preface. Electr. Notes Theor. Comput. Sci. 68(4): 483 (2002)

Orna Grumberg: Different directions in parallel and distributed model checking (invited talk). Electr. Notes Theor. Comput. Sci. 68(4): 485 (2002)

Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster: A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits. Formal Methods in System Design 21(3): 317-338 (2002)

Karen Yorav, Orna Grumberg: Syntax-directed model checking of sequential programs. J. Log. Algebr. Program. 52-53: 129-162 (2002)

Sharon Barner, Orna Grumberg: Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. CAV 2002: 93-106

Shmuel Katz, Orna Grumberg: A Framework for Translating Models and Specifications. IFM 2002: 145-164

Katerina Korenblat, Orna Grumberg, Shmuel Katz: Translations between Textual Transition Systems and Petri Nets. IFM 2002: 339-359

Doron Bustan, Orna Grumberg: Applicability of Fair Simulation. TACAS 2002: 401-414

Edmund M. Clarke, Orna Grumberg, Doron Peled: Model checking. MIT Press 2001, isbn 978-0-262-03270-4, pp. I-XIV, 1-314

Orna Grumberg: Introduction: Special Issue on CAV '97. Formal Methods in System Design 18(2): 95 (2001)

Orna Grumberg, Robert P. Kurshan: Which Branching-Time Properties are Effectively Linear? J. Log. Comput. 11(2): 201-228 (2001)

Orna Grumberg, Tamir Heyman, Assaf Schuster: Distributed Symbolic Model Checking for µ-Calculus. CAV 2001: 350-362

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith: Progress on the State Explosion Problem in Model Checking. Informatics 2001: 176-194

Sérgio Vale Aguiar Campos, Edmund M. Clarke, Orna Grumberg: Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. Formal Methods in System Design 17(2): 163-192 (2000)

Doron Bustan, Orna Grumberg: Simulation Based Minimization. CADE 2000: 255-270

Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster: Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. CAV 2000: 20-35

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith: Counterexample-Guided Abstraction Refinement. CAV 2000: 154-169

Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster: Scalable Distributed On-the-Fly Symbolic Model Checking. FMCAD 2000: 390-404

Alessandro Cimatti, Orna Grumberg: Preface. Electr. Notes Theor. Comput. Sci. 23(2): 127-128 (1999)

Edmund M. Clarke, Orna Grumberg, Marius Minea, Doron Peled: State Space Reduction Using Partial Order Techniques. STTT 2(3): 279-287 (1999)

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

Jürgen Bohn, Werner Damm, Orna Grumberg, Hardi Hungar, Karen Laster: First-Order-CTL Model Checking. FSTTCS 1998: 283-294

Karen Laster, Orna Grumberg: Modular Model Checking of Software. TACAS 1998: 20-35

Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi: Another Look at LTL Model Checking. Formal Methods in System Design 10(1): 47-71 (1997)

Dennis Dams, Rob Gerth, Orna Grumberg: Abstract Interpretation of Reactive Systems. ACM Trans. Program. Lang. Syst. 19(2): 253-291 (1997)

Edmund M. Clarke, Orna Grumberg, Somesh Jha: Verifying Parameterized Networks. ACM Trans. Program. Lang. Syst. 19(5): 726-750 (1997)

Orna Grumberg (Ed.): Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings. Lecture Notes in Computer Science 1254, Springer 1997, isbn 3-540-63166-6

Orna Kupferman, Orna Grumberg: Branching-Time Temporal Logic and Tree Automata. Inf. Comput. 125(1): 62-69 (1996)

Limor Fix, Orna Grumberg: Verification of Temporal Properties. J. Log. Comput. 6(3): 343-361 (1996)

Orna Kupferman, Orna Grumberg: Buy One, Get One Free!!! J. Log. Comput. 6(4): 523-539 (1996)

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

Edmund M. Clarke, Orna Grumberg, David E. Long: Model checking. NATO ASI DPD 1996: 305-349

Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness: Verification of the Futurebus+ Cache Coherence Protocol. Formal Methods in System Design 6(2): 217-232 (1995)

Hardi Hungar, Orna Grumberg, Werner Damm: What if model checking must be truly symbolic. CHARME 1995: 1-20

Edmund M. Clarke, Orna Grumberg, Somesh Jha: Veryfying Parameterized Networks using Abstraction and Regular Languages. CONCUR 1995: 395-407

Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995: 427-432

Girish Bhat, Rance Cleaveland, Orna Grumberg: Efficient On-the-Fly Model Checking for CTL*. LICS 1995: 388-397

Limor Fix, Nissim Francez, Orna Grumberg: Program Composition via Unification. Theor. Comput. Sci. 131(1): 139-179 (1994)

Orna Grumberg, David E. Long: Model Checking and Modular Verification. ACM Trans. Program. Lang. Syst. 16(3): 843-871 (1994)

Edmund M. Clarke, Orna Grumberg, David E. Long: Model Checking and Abstraction. ACM Trans. Program. Lang. Syst. 16(5): 1512-1542 (1994)

Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi: Another Look at LTL Model Checking. CAV 1994: 415-427

Orna Grumberg, Robert P. Kurshan: How Linear Can Branching-Time Be? ICTL 1994: 180-194

Orna Bernholtz, Orna Grumberg: Buy One, Get One Free!!! ICTL 1994: 210-224

Paul C. Attie, Nissim Francez, Orna Grumberg: Fairness and Hyperfairness in Multi-Party Interactions. Distributed Computing 6(4): 245-254 (1993)

Hana De-Leon, Orna Grumberg: Modular Abstractions for Verifying Real-Time Distributed Systems. Formal Methods in System Design 2(1): 7-43 (1993)

Dennis Dams, Orna Grumberg, Rob Gerth: Generation of Reduced Models for Checking Fragments of CTL. CAV 1993: 479-490

Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness: Verification of the Futurebus+ Cache Coherence Protocol. CHDL 1993: 15-30

Orna Bernholtz, Orna Grumberg: Branching Time Temporal Logic and Amorphous Tree Automata. CONCUR 1993: 262-277

Edmund M. Clarke, Orna Grumberg, David E. Long: Verification Tools for Finite-State Concurrent Systems. REX School/Symposium 1993: 124-175

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

Hana De-Leon, Orna Grumberg: Modular Abstractions for Verifying Real-Time Distributed Systems. CAV 1992: 2-15

Limor Fix, Nissim Francez, Orna Grumberg: Program Composition via Unification. ICALP 1992: 672-684

Edmund M. Clarke, Orna Grumberg, David E. Long: Model Checking and Abstraction. POPL 1992: 342-354

Orna Grumberg, David E. Long: Model Checking and Modular Verification. CONCUR 1991: 250-265

Limor Fix, Nissim Francez, Orna Grumberg: Program Composition and Modular Verification. ICALP 1991: 93-114

Gil Shurek, Orna Grumberg: The Modular Framework of Computer-Aided Verification. CAV 1990: 214-223

Paul C. Attie, Nissim Francez, Orna Grumberg: Fairness and Hyperfairness in Multi-Party Interactions. POPL 1990: 292-305

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

Ze'ev Shtadler, Orna Grumberg: Network Grammars, Communication Behaviors and Automatic Verification. Automatic Verification Methods for Finite State Systems 1989: 151-165

Edmund M. Clarke, Orna Grumberg, Robert P. Kurshan: A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. Logic at Botik 1989: 81-90

Ran Rinat, Nissim Francez, Orna Grumberg: Infinite Trees, Markings and Well-Foundedness. Inf. Comput. 79(2): 131-154 (1988)

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

Edmund M. Clarke, Orna Grumberg: Avoiding The State Explosion Problem in Temporal Logic Model Checking. PODC 1987: 294-303

Michael C. Browne, Edmund M. Clarke, Orna Grumberg: Characterizing Kripke Structures in Temporal Logic. TAPSOFT, Vol.1 1987: 256-270

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

Orna Grumberg, Nissim Francez, Shmuel Katz: A Complete Rule for Equifair Termination. J. Comput. Syst. Sci. 33(3): 313-332 (1986)

Ran Rinat, Nissim Francez, Orna Grumberg: Infinite Trees, Markings and Well Foundedness. CAAP 1986: 238-253

Edmund M. Clarke, Orna Grumberg, Michael C. Browne: Reasoning About Networks With Many Identical Finite-State Processes. PODC 1986: 240-248

Orna Grumberg, Nissim Francez, Johann A. Makowsky, Willem P. de Roever: A Proof Rule for Fair Termination of Guarded Commands. Information and Control 66(1/2): 83-102 (1985)

Nissim Francez, Orna Grumberg, Shmuel Katz, Amir Pnueli: Proving Termination of Prolog Programs. Logic of Programs 1985: 89-105

Orna Grumberg, Nissim Francez, Shmuel Katz: Fail Termination of Communicating Processe. PODC 1984: 254-265

Orna Grumberg, Nissim Francez, Shmuel Katz: A Compete Proof Rule for Strong Equifair Termination. Logic of Programs 1983: 257-278