Orna Grumberg - RankMe

181 papers A* 29A 7B 29C 2Misc 1Journal 60Unranked 36

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	CTL Principles of Formal Quantitative Analysis Mishel Carelli, Orna Grumberg
2025	J	`jnl`	STACHE: Local Black-Box Explanations for Reinforcement Learning Policies. CoRR Andrew Elashkin, Orna Grumberg
2025	J	`jnl`	Variable automata over infinite alphabets. Formal Methods Syst. Des. Orna Grumberg, Orna Kupferman, Sarai Sheinvald
2024	—	`conf`	CTL ATVA (2) Mishel Carelli, Orna Grumberg
2024	J	`jnl`	CTL* Verification and Synthesis using Existential Horn Clauses. CoRR Mishel Carelli, Orna Grumberg
2023	—	`conf`	Condition Synthesis Realizability via Constrained Horn Clauses. NFM Bat-Chen Rothenberg, Orna Grumberg, Yakir Vizel, Eytan Singher
2023	B	`conf`	Structure-Guided Solution of Constrained Horn Clauses. ATVA Omer Rappoport, Orna Grumberg, Yakir Vizel
2022	J	`jnl`	Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties (full version). CoRR Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald
2022	J	`jnl`	Assume, guarantee or repair: a regular framework for non regular properties. Int. J. Softw. Tools Technol. Transf. Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald
2022	—	`conf`	Automated Program Repair Using Formal Verification Techniques. Principles of Systems Design Hadar Frenkel, Orna Grumberg, Bat-Chen Rothenberg, Sarai Sheinvald
2022	J	`jnl`	Edmund Melson Clarke, Jr. (1945-2020). Formal Methods Syst. Des. Sicun Gao, Orna Grumberg, Paolo Zuliani
2021	B	`conf`	Compositional Model Checking for Multi-properties. VMCAI Ohad Goudsmid, Orna Grumberg, Sarai Sheinvald
2021	J	`jnl`	Modular Verification of Concurrent Programs via Sequential Model Checking. CoRR Dan Rasin, Orna Grumberg, Sharon Shoham
2020	—	`conf`	Assume, Guarantee or Repair. TACAS (1) Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald
2020	—	`conf`	Must Fault Localization for Program Repair. CAV (2) Bat-Chen Rothenberg, Orna Grumberg
2019	J	`jnl`	An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains. J. Autom. Reason. Hadar Frenkel, Orna Grumberg, Sarai Sheinvald
2019	—	`conf`	Topology-Agnostic Runtime Detection of OSPF Routing Attacks. CNS Nurit Devir, Orna Grumberg, Shaul Markovitch, Gabi Nakibly
2018	—	`ch.`	Abstraction and Abstraction Refinement. Handbook of Model Checking Dennis Dams, Orna Grumberg
2018	J	`jnl`	Automated circular assume-guarantee reasoning. Formal Aspects Comput. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
2018	—	`book`	Model checking, 2nd Edition. Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, Helmut Veith
2018	B	`conf`	Modular Verification of Concurrent Programs via Sequential Model Checking. ATVA Dan Rasin, Orna Grumberg, Sharon Shoham
2018	—	`conf`	Program repair that learns from mistakes. ICSE (Companion Volume) Bat-Chen Rothenberg, Orna Grumberg
2017	—	`conf`	An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data. NFM Hadar Frenkel, Orna Grumberg, Sarai Sheinvald
2017	J	`jnl`	Formal Black-Box Analysis of Routing Protocol Implementations. CoRR Adi Sosnovich, Orna Grumberg, Gabi Nakibly
2017	B	`conf`	Modular Demand-Driven Analysis of Semantic Difference for Program Versions. SAS Anna Trostanetski, Orna Grumberg, Daniel Kroening
2016	J	`jnl`	A framework for compositional verification of multi-valued systems via abstraction-refinement. Inf. Comput. Yael Meller, Orna Grumberg, Sharon Shoham
2016	—	`conf`	Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. CAV (1) Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
2016	—	`book`	Dependable Software Systems Engineering Dependable Software Systems Engineering Javier Esparza, Orna Grumberg, Salomon Sickert
2016	—	`ch.`	Learning-Based Compositional Model Checking of Behavioral UML Systems. Dependable Software Systems Engineering Orna Grumberg, Yael Meller
2016	B	`conf`	Sound and Complete Mutation-Based Program Repair. FM Bat-Chen Rothenberg, Orna Grumberg
2016	J	`jnl`	Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201). Dagstuhl Reports Julian Dolby, Orna Grumberg, Peter Müller, Omer Tripp
2015	B	`conf`	Analyzing Internet Routing Security Using Model Checking. LPAR Adi Sosnovich, Orna Grumberg, Gabi Nakibly
2015	B	`conf`	Automated Circular Assume-Guarantee Reasoning. FM Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
2015	—	`conf`	Learning-Based Compositional Model Checking of Behavioral UML Systems. FACS Yael Meller, Orna Grumberg, Karen Yorav
2014	B	`conf`	A Game-Theoretic Approach to Simulation of Data-Parameterized Systems. ATVA Orna Grumberg, Orna Kupferman, Sarai Sheinvald
2014	—	`ch.`	SAT-based Model Checking: Interpolation, IC3, and Beyond. Software Systems Safety Orna Grumberg, Sharon Shoham, Yakir Vizel
2014	—	`book`	Software Systems Safety Software Systems Safety Orna Grumberg, Helmut Seidl, Maximilian Irlbeck
2014	B	`conf`	Verifying Behavioral UML Systems via CEGAR. IFM Yael Meller, Orna Grumberg, Karen Yorav
2013	B	`conf`	An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. ATVA Orna Grumberg, Orna Kupferman, Sarai Sheinvald
2013	A*	`conf`	Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems. CAV Adi Sosnovich, Orna Grumberg, Gabi Nakibly
2013	A	`conf`	Intertwined Forward-Backward Reachability Analysis Using Interpolants. TACAS Yakir Vizel, Orna Grumberg, Sharon Shoham
2012	J	`jnl`	2010 CAV award announcement. Formal Methods Syst. Des. Orna Grumberg, Moshe Y. Vardi, Joseph Sifakis, Rajeev Alur
2012	B	`conf`	Applying Software Model Checking Techniques for Behavioral UML Models. FM Orna Grumberg, Yael Meller, Karen Yorav
2012	B	`conf`	Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD Yakir Vizel, Orna Grumberg, Sharon Shoham
2012	B	`conf`	Model Checking Systems and Specifications with Parameterized Atomic Propositions. ATVA Orna Grumberg, Orna Kupferman, Sarai Sheinvald
2012	—	`ch.`	Model Checking: From BDDs to Interpolation. Software Safety and Security Orna Grumberg
2012	J	`jnl`	Multi-valued model checking games. J. Comput. Syst. Sci. Sharon Shoham, Orna Grumberg
2012	—	`book`	Software Safety and Security - Tools for Analysis and Verification Software Safety and Security Tobias Nipkow, Orna Grumberg, Benedikt Hauptmann
2011	J	`jnl`	Learning to Order BDD Variables in Verification CoRR Orna Grumberg, Shlomi Livne, Shaul Markovitch
2010	—	`ch.`	2-Valued and 3-Valued Abstraction-Refinement in Model Checking. Logics and Languages for Reliability and Security Orna Grumberg
2010	J	`jnl`	2009 CAV award announcement. Formal Methods Syst. Des. Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi
2010	J	`jnl`	Compositional verification and 3-valued abstractions join forces. Inf. Comput. Sharon Shoham, Orna Grumberg
2010	—	`book`	Logics and Languages for Reliability and Security Logics and Languages for Reliability and Security Javier Esparza, Bernd Spanfelner, Orna Grumberg
2010	C	`conf`	Variable Automata over Infinite Alphabets. LATA Orna Grumberg, Orna Kupferman, Sarai Sheinvald
2009	B	`conf`	3-Valued Abstraction for (Bounded) Model Checking. ATVA Orna Grumberg
2009	B	`conf`	A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. ATVA Yael Meller, Orna Grumberg, Sharon Shoham
2009	J	`jnl`	Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Formal Methods Syst. Des. Himanshu Jain, Edmund M. Clarke, Orna Grumberg
2009	—	`conf`	Hybrid BDD and All-SAT Method for Model Checking. Languages: From Formal to Natural Avi Yadgar, Orna Grumberg, Assaf Schuster
2009	B	`conf`	Interpolation-sequence based model checking. FMCAD Yakir Vizel, Orna Grumberg
2009	—	`ed.`	Languages: From Formal to Natural, Essays Dedicated to Nissim Francez on the Occasion of His 65th Birthday Languages: From Formal to Natural Orna Grumberg, Michael Kaminski, Shmuel Katz, Shuly Wintner
2009	J	`jnl`	Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification. Int. J. Softw. Tools Technol. Transf. Michael Huth, Orna Grumberg
2009	J	`jnl`	The 2008 CAV Award citation. Formal Methods Syst. Des. Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi
2008	—	`ed.`	25 Years of Model Checking - History, Achievements, Perspectives 25 Years of Model Checking Orna Grumberg, Helmut Veith
2008	J	`jnl`	3-Valued abstraction: More precision at less cost. Inf. Comput. Sharon Shoham, Orna Grumberg
2008	A	`conf`	Efficient Automatic STE Refinement Using Responsibility. TACAS Hana Chockler, Orna Grumberg, Avi Yadgar
2008	A*	`conf`	Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. CAV Himanshu Jain, Edmund M. Clarke, Orna Grumberg
2007	B	`conf`	3-Valued Circuit SAT for STE with Automatic Refinement. ATVA Orna Grumberg, Assaf Schuster, Avi Yadgar
2007	B	`conf`	A New Approach to Bounded Model Checking for Branching Time Logics. ATVA Rotem Oshman, Orna Grumberg
2007	J	`jnl`	A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Log. Sharon Shoham, Orna Grumberg
2007	B	`conf`	Compositional Verification and 3-Valued Abstractions Join Forces. SAS Sharon Shoham, Orna Grumberg
2007	A	`ed.`	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 TACAS Orna Grumberg, Michael Huth
2007	J	`jnl`	VeriTech: a framework for translating among model description notations. Int. J. Softw. Tools Technol. Transf. Orna Grumberg, Shmuel Katz
2007	J	`jnl`	Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. Int. J. Found. Comput. Sci. Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster
2007	J	`jnl`	When not losing is better than winning: Abstraction and refinement for the full mu-calculus. Inf. Comput. Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham
2006	A*	`conf`	3-Valued Abstraction: More Precision at Less Cost. LICS Sharon Shoham, Orna Grumberg
2006	J	`jnl`	A work-efficient distributed algorithm for reachability analysis. Formal Methods Syst. Des. Orna Grumberg, Tamir Heyman, Assaf Schuster
2006	A*	`conf`	Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. CAV Rachel Tzoref, Orna Grumberg
2005	—	`conf`	Abstraction and Refinement in Model Checking. FMCO Orna Grumberg
2005	—	`conf`	Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. CHARME Orna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster
2005	A*	`conf`	Bounded Model Checking of Concurrent Programs. CAV Ishai Rabinovitz, Orna Grumberg
2005	J	`jnl`	Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. Formal Methods Syst. Des. Sharon Barner, Orna Grumberg
2005	J	`jnl`	Distributed Symbolic Model Checking for µ-Calculus. Formal Methods Syst. Des. Orna Grumberg, Tamir Heyman, Assaf Schuster
2005	J	`jnl`	Introductory paper. Int. J. Softw. Tools Technol. Transf. Lubos Brim, Orna Grumberg
2005	B	`conf`	Multi-valued Model Checking Games. ATVA Sharon Shoham, Orna Grumberg
2005	A*	`conf`	Proof-guided underapproximation-widening for multi-process systems. POPL Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald
2005	—	`conf`	Regular Vacuity. CHARME Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi
2005	B	`conf`	State/Event Software Verification for Branching-Time Specifications. IFM Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith
2005	B	`conf`	Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. ATVA Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster
2004	J	`jnl`	Applicability of fair simulation. Inf. Comput. Doron Bustan, Orna Grumberg
2004	B	`conf`	Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. FMCAD Orna Grumberg, Assaf Schuster, Avi Yadgar
2004	A	`conf`	Monotonic Abstraction-Refinement for CTL. TACAS Sharon Shoham, Orna Grumberg
2004	J	`jnl`	Static Analysis for State-Space Reductions Preserving Temporal Logics. Formal Methods Syst. Des. Karen Yorav, Orna Grumberg
2004	J	`jnl`	Test sequence generation and model checking using dynamic transition relations. Int. J. Softw. Tools Technol. Transf. Sérgio Vale Aguiar Campos, Orna Grumberg, Karen Yorav, Fady Copty
2003	—	`ed.`	12th International Workshop on Functional and Constraint Logic Programming, WFLP 2003, in connection with RDP'03, Federated Conference on Rewriting, Deduction and Programming, Boulder, Colorado, USA, July 14, 2003 WFLP Lubos Brim, Orna Grumberg
2003	—	`ed.`	2nd International Workshop on Parallel and Distributed Model Checking, PDMC 2003, Satellite Workshop of CAV 2003, Boulder, Colorado, USA, July 13, 2003 PDMC@CAV Lubos Brim, Orna Grumberg
2003	A*	`conf`	A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. CAV Sharon Shoham, Orna Grumberg
2003	A*	`conf`	A Work-Efficient Distributed Algorithm for Reachability Analysis. CAV Orna Grumberg, Tamir Heyman, Assaf Schuster
2003	J	`jnl`	Counterexample-guided abstraction refinement for symbolic model checking. J. ACM Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
2003	A*	`conf`	Enhanced Vacuity Detection in Linear Temporal Logic. CAV Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi
2003	C	`conf`	High Level Verification of Control Intensive Systems Using Predicate Abstraction. MEMOCODE Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang
2003	J	`jnl`	Learning to Order BDD Variables in Verification. J. Artif. Intell. Res. Orna Grumberg, Shlomi Livne, Shaul Markovitch
2003	A*	`conf`	Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. CAV Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang
2003	—	`conf`	Preface. PDMC@CAV Lubos Brim, Orna Grumberg
2003	J	`jnl`	Scalable distributed on-the-fly symbolic model checking. Int. J. Softw. Tools Technol. Transf. Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster
2003	J	`jnl`	Simulation-based minimazation. ACM Trans. Comput. Log. Doron Bustan, Orna Grumberg
2002	B	`conf`	A Framework for Translating Models and Specifications. IFM Shmuel Katz, Orna Grumberg
2002	J	`jnl`	A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits. Formal Methods Syst. Des. Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster
2002	A	`conf`	Applicability of Fair Simulation. TACAS Doron Bustan, Orna Grumberg
2002	A*	`conf`	Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. CAV Sharon Barner, Orna Grumberg
2002	—	`conf`	Different directions in parallel and distributed model checking (invited talk). PDMC@CONCUR Orna Grumberg
2002	—	`ed.`	Parallel and Distributed Model Checking, PDMC 2002, Satellite Workshop of CONCUR 2002, Brno, Czech Republic, August 19, 2002 PDMC@CONCUR Lubos Brim, Orna Grumberg
2002	—	`conf`	Preface. PDMC@CONCUR Lubos Brim, Orna Grumberg
2002	J	`jnl`	Syntax-directed model checking of sequential programs. J. Log. Algebraic Methods Program. Karen Yorav, Orna Grumberg
2002	B	`conf`	Translations between Textual Transition Systems and Petri Nets. IFM Katerina Korenblat, Orna Grumberg, Shmuel Katz
2001	A*	`conf`	Distributed Symbolic Model Checking for µ-Calculus. CAV Orna Grumberg, Tamir Heyman, Assaf Schuster
2001	J	`jnl`	Introduction: Special Issue on CAV '97. Formal Methods Syst. Des. Orna Grumberg
2001	—	`book`	Model checking, 1st Edition. Edmund M. Clarke, Orna Grumberg, Doron A. Peled
2001	Misc	`conf`	Progress on the State Explosion Problem in Model Checking. Informatics Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
2001	J	`jnl`	Which Branching-Time Properties are Effectively Linear? J. Log. Comput. Orna Grumberg, Robert P. Kurshan
2000	A*	`conf`	Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. CAV Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster
2000	A*	`conf`	Counterexample-Guided Abstraction Refinement. CAV Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
2000	B	`conf`	Scalable Distributed On-the-Fly Symbolic Model Checking. FMCAD Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster
2000	J	`jnl`	Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. Formal Methods Syst. Des. Sérgio Vale Aguiar Campos, Edmund M. Clarke, Orna Grumberg
2000	A	`conf`	Simulation Based Minimization. CADE Doron Bustan, Orna Grumberg
1999	—	`conf`	"Have I written enough Properties?" - A Method of Comparison between Specification and Implementation. CHARME Sagi Katz, Orna Grumberg, Daniel Geist
1999	—	`ed.`	First International Workshop on Symbolic Model Checking, SMC 1999, associated to FLoC'99, the 1999 Federated Logic Conference, Trento, Italy, July 6, 1999 SMC@FLoC Alessandro Cimatti, Orna Grumberg
1999	—	`conf`	Preface. SMC@FLoC Alessandro Cimatti, Orna Grumberg
1999	J	`jnl`	State Space Reduction Using Partial Order Techniques. Int. J. Softw. Tools Technol. Transf. Edmund M. Clarke, Orna Grumberg, Marius Minea, Doron A. Peled
1998	—	`conf`	First-Order-CTL Model Checking. FSTTCS Jürgen Bohn, Werner Damm, Orna Grumberg, Hardi Hungar, Karen Laster
1998	A	`conf`	Modular Model Checking of Software. TACAS Karen Laster, Orna Grumberg
1997	J	`jnl`	Abstract Interpretation of Reactive Systems. ACM Trans. Program. Lang. Syst. Dennis Dams, Rob Gerth, Orna Grumberg
1997	J	`jnl`	Another Look at LTL Model Checking. Formal Methods Syst. Des. Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi
1997	A*	`ed.`	Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings CAV Orna Grumberg
1997	J	`jnl`	Verifying Parameterized Networks. ACM Trans. Program. Lang. Syst. Edmund M. Clarke, Orna Grumberg, Somesh Jha
1996	J	`jnl`	Branching-Time Temporal Logic and Tree Automata. Inf. Comput. Orna Kupferman, Orna Grumberg
1996	J	`jnl`	Buy One, Get One Free!!! J. Log. Comput. Orna Kupferman, Orna Grumberg
1996	—	`conf`	Model checking. NATO ASI DPD Edmund M. Clarke, Orna Grumberg, David E. Long
1996	A*	`conf`	Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. CAV Sérgio Vale Aguiar Campos, Orna Grumberg
1996	J	`jnl`	Verification of Temporal Properties. J. Log. Comput. Limor Fix, Orna Grumberg
1995	A*	`conf`	Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao
1995	A*	`conf`	Efficient On-the-Fly Model Checking for CTL* LICS Girish Bhat, Rance Cleaveland, Orna Grumberg
1995	J	`jnl`	Verification of the Futurebus+ Cache Coherence Protocol. Formal Methods Syst. Des. Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness
1995	B	`conf`	Veryfying Parameterized Networks using Abstraction and Regular Languages. CONCUR Edmund M. Clarke, Orna Grumberg, Somesh Jha
1995	—	`conf`	What if model checking must be truly symbolic. CHARME Hardi Hungar, Orna Grumberg, Werner Damm
1994	A*	`conf`	Another Look at LTL Model Checking. CAV Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi
1994	—	`conf`	Buy One, Get One Free!!! ICTL Orna Bernholtz, Orna Grumberg
1994	—	`conf`	How Linear Can Branching-Time Be? ICTL Orna Grumberg, Robert P. Kurshan
1994	J	`jnl`	Model Checking and Abstraction. ACM Trans. Program. Lang. Syst. Edmund M. Clarke, Orna Grumberg, David E. Long
1994	J	`jnl`	Model Checking and Modular Verification. ACM Trans. Program. Lang. Syst. Orna Grumberg, David E. Long
1994	J	`jnl`	Program Composition via Unification. Theor. Comput. Sci. Limor Fix, Nissim Francez, Orna Grumberg
1993	B	`conf`	Branching Time Temporal Logic and Amorphous Tree Automata. CONCUR Orna Bernholtz, Orna Grumberg
1993	J	`jnl`	Fairness and Hyperfairness in Multi-Party Interactions. Distributed Comput. Paul C. Attie, Nissim Francez, Orna Grumberg
1993	A*	`conf`	Generation of Reduced Models for Checking Fragments of CTL. CAV Dennis Dams, Orna Grumberg, Rob Gerth
1993	J	`jnl`	Modular Abstractions for Verifying Real-Time Distributed Systems. Formal Methods Syst. Des. Hana De-Leon, Orna Grumberg
1993	—	`conf`	Verification Tools for Finite-State Concurrent Systems. REX School/Symposium Edmund M. Clarke, Orna Grumberg, David E. Long
1993	—	`conf`	Verification of the Futurebus+ Cache Coherence Protocol. CHDL Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness
1992	J	`jnl`	A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. J. Log. Comput. Edmund M. Clarke, Orna Grumberg, Robert P. Kurshan
1992	A*	`conf`	Model Checking and Abstraction. POPL Edmund M. Clarke, Orna Grumberg, David E. Long
1992	A*	`conf`	Modular Abstractions for Verifying Real-Time Distributed Systems. CAV Hana De-Leon, Orna Grumberg
1992	A*	`conf`	Program Composition via Unification. ICALP Limor Fix, Nissim Francez, Orna Grumberg
1991	B	`conf`	Model Checking and Modular Verification. CONCUR Orna Grumberg, David E. Long
1991	A*	`conf`	Program Composition and Modular Verification. ICALP Limor Fix, Nissim Francez, Orna Grumberg
1990	A*	`conf`	Fairness and Hyperfairness in Multi-Party Interactions. POPL Paul C. Attie, Nissim Francez, Orna Grumberg
1990	—	`conf`	Sematics-Driven Decompositions for the Verification of Distributed Programs. Programming Concepts and Methods Limor Fix, Nissim Francez, Orna Grumberg
1990	A*	`conf`	The Modular Framework of Computer-Aided Verification. CAV Gil Shurek, Orna Grumberg
1990	—	`conf`	The Modular Framework of Computer-Aided Verification. CAV (DIMACS/AMS volume) Gil Shurek, Orna Grumberg
1989	—	`conf`	A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. Logic at Botik Edmund M. Clarke, Orna Grumberg, Robert P. Kurshan
1989	—	`conf`	Network Grammars, Communication Behaviors and Automatic Verification. Automatic Verification Methods for Finite State Systems Ze'ev Shtadler, Orna Grumberg
1989	J	`jnl`	Reasoning about Networks with Many Identical Finite State Processes Inf. Comput. Michael C. Browne, Edmund M. Clarke, Orna Grumberg
1988	J	`jnl`	Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theor. Comput. Sci. Michael C. Browne, Edmund M. Clarke, Orna Grumberg
1988	J	`jnl`	Infinite Trees, Markings and Well-Foundedness Inf. Comput. Ran Rinat, Nissim Francez, Orna Grumberg
1987	A*	`conf`	Avoiding The State Explosion Problem in Temporal Logic Model Checking. PODC Edmund M. Clarke, Orna Grumberg
1987	—	`conf`	Characterizing Kripke Structures in Temporal Logic. TAPSOFT, Vol.1 Michael C. Browne, Edmund M. Clarke, Orna Grumberg
1987	—	`conf`	The Model Checking Problem for Concurrent Systems with Many Similar Processes. Temporal Logic in Specification Edmund M. Clarke, Orna Grumberg
1986	J	`jnl`	A Complete Rule for Equifair Termination. J. Comput. Syst. Sci. Orna Grumberg, Nissim Francez, Shmuel Katz
1986	—	`conf`	Infinite Trees, Markings and Well Foundedness. CAAP Ran Rinat, Nissim Francez, Orna Grumberg
1986	A*	`conf`	Reasoning About Networks With Many Identical Finite-State Processes. PODC Edmund M. Clarke, Orna Grumberg, Michael C. Browne
1985	J	`jnl`	A Proof Rule for Fair Termination of Guarded Commands Inf. Control. Orna Grumberg, Nissim Francez, Johann A. Makowsky, Willem P. de Roever
1985	—	`conf`	Proving Termination of Prolog Programs. Logic of Programs Nissim Francez, Orna Grumberg, Shmuel Katz, Amir Pnueli
1984	A*	`conf`	Fail Termination of Communicating Processe. PODC Orna Grumberg, Nissim Francez, Shmuel Katz
1983	—	`conf`	A Compete Proof Rule for Strong Equifair Termination. Logic of Programs Orna Grumberg, Nissim Francez, Shmuel Katz