| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Sharon Shoham, Orna Grumberg |
Multi-valued model checking games.  |
J. Comput. Syst. Sci.  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Moshe Y. Vardi, Joseph Sifakis, Rajeev Alur |
2010 CAV award announcement. |
Formal Methods in System Design |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Shlomi Livne, Shaul Markovitch |
Learning to Order BDD Variables in Verification |
CoRR |
2011 |
DBLP BibTeX RDF |
|
| 1 | Sharon Shoham, Orna Grumberg |
Compositional verification and 3-valued abstractions join forces. |
Inf. Comput. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi |
2009 CAV award announcement. |
Formal Methods in System Design |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Javier Esparza, Bernd Spanfelner, Orna Grumberg (eds.) |
Logics and Languages for Reliability and Security |
|
2010 |
DBLP BibTeX RDF |
|
| 1 | Orna Grumberg |
2-Valued and 3-Valued Abstraction-Refinement in Model Checking. |
Logics and Languages for Reliability and Security |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
Variable Automata over Infinite Alphabets. |
LATA |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Huth, Orna Grumberg |
Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification. |
STTT |
2009 |
DBLP DOI BibTeX RDF |
Bounded reachability, Bit-vector arithmetic, Abstraction, Asynchronous systems, Decision diagrams, Memory models, Decision problems |
| 1 | Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi |
The 2008 CAV Award citation. |
Formal Methods in System Design |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Himanshu Jain, Edmund M. Clarke, Orna Grumberg |
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. |
Formal Methods in System Design |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Yakir Vizel, Orna Grumberg |
Interpolation-sequence based model checking. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg |
3-Valued Abstraction for (Bounded) Model Checking. |
ATVA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Yael Meller, Orna Grumberg, Sharon Shoham |
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. |
ATVA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Avi Yadgar, Orna Grumberg, Assaf Schuster |
Hybrid BDD and All-SAT Method for Model Checking. |
Languages: From Formal to Natural |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
Languages: From Formal to Natural |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Shoham, Orna Grumberg |
3-Valued abstraction: More precision at less cost. |
Inf. Comput. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Hana Chockler, Orna Grumberg, Avi Yadgar |
Efficient Automatic STE Refinement Using Responsibility. |
TACAS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Helmut Veith (eds.) |
25 Years of Model Checking - History, Achievements, Perspectives |
25 Years of Model Checking |
2008 |
DBLP BibTeX RDF |
|
| 1 | Himanshu Jain, Edmund M. Clarke, Orna Grumberg |
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Shoham, Orna Grumberg |
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. |
ACM Trans. Comput. Log. |
2007 |
DBLP DOI BibTeX RDF |
3-valued semantics, Model checking games, Temporal logic, CTL, Counterexamples, Abstraction-Refinement |
| 1 | Orna Grumberg, Shmuel Katz |
VeriTech: a framework for translating among model description notations. |
STTT |
2007 |
DBLP DOI BibTeX RDF |
Translating model notations, Incompatibilities in translations Faithful translations, Additional information about translations |
| 1 | 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 |
TACAS |
2007 |
DBLP BibTeX RDF |
|
| 1 | Orna Grumberg, Assaf Schuster, Avi Yadgar |
3-Valued Circuit SAT for STE with Automatic Refinement. |
ATVA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Rotem Oshman, Orna Grumberg |
A New Approach to Bounded Model Checking for Branching Time Logics. |
ATVA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Shoham, Orna Grumberg |
Compositional Verification and 3-Valued Abstractions Join Forces. |
SAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Tamir Heyman, Assaf Schuster |
A work-efficient distributed algorithm for reachability analysis. |
Formal Methods in System Design |
2006 |
DBLP DOI BibTeX RDF |
Distributed reachability, Distributed BDDs, Symbolic model checking |
| 1 | Rachel Tzoref, Orna Grumberg |
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Shoham, Orna Grumberg |
3-Valued Abstraction: More Precision at Less Cost. |
LICS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Lubos Brim, Orna Grumberg |
Introductory paper. |
STTT |
2005 |
DBLP DOI BibTeX RDF |
Parallel verification, Model checking, Distributed computing |
| 1 | Sharon Barner, Orna Grumberg |
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. |
Formal Methods in System Design |
2005 |
DBLP DOI BibTeX RDF |
under-approximation, symbolic model checking, hints, symmetry reduction |
| 1 | Orna Grumberg, Tamir Heyman, Assaf Schuster |
Distributed Symbolic Model Checking for µ-Calculus. |
Formal Methods in System Design |
2005 |
DBLP DOI BibTeX RDF |
model checking, distributed, hardware verification, symbolic, Mu-calculus |
| 1 | Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald |
Proof-guided underapproximation-widening for multi-process systems. |
POPL |
2005 |
DBLP DOI BibTeX RDF |
SAT proofs, underapproximation-widening, abstraction, software verification, bounded model checking |
| 1 | Sharon Shoham, Orna Grumberg |
Multi-valued Model Checking Games. |
ATVA |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster |
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. |
ATVA |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg |
Abstraction and Refinement in Model Checking. |
FMCO |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi |
Regular Vacuity. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster |
Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
Concurrent Software Model Checking, State/Event-based Verification, Branching-time Temporal Logic, Automated Abstraction Refinement |
| 1 | Ishai Rabinovitz, Orna Grumberg |
Bounded Model Checking of Concurrent Programs. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham |
Don't Know in the µ-Calculus. |
VMCAI |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Doron Bustan, Orna Grumberg |
Applicability of fair simulation. |
Inf. Comput. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Sérgio Vale Aguiar Campos, Orna Grumberg, Karen Yorav, Copty Fady |
Test sequence generation and model checking using dynamic transition relations. |
STTT |
2004 |
DBLP DOI BibTeX RDF |
Binary decision diagrams, Symbolic model checking, Test sequence generation |
| 1 | Karen Yorav, Orna Grumberg |
Static Analysis for State-Space Reductions Preserving Temporal Logics. |
Formal Methods in System Design |
2004 |
DBLP DOI BibTeX RDF |
path reduction, (partially) dead variable reduction, temporal logic preservation, static analysis |
| 1 | Sharon Shoham, Orna Grumberg |
Monotonic Abstraction-Refinement for CTL. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Assaf Schuster, Avi Yadgar |
Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Lubos Brim, Orna Grumberg |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith |
Counterexample-guided abstraction refinement for symbolic model checking. |
J. ACM |
2003 |
DBLP DOI BibTeX RDF |
temporal logic, Abstraction, symbolic model checking, hardware verification |
| 1 | Orna Grumberg, Shlomi Livne, Shaul Markovitch |
Learning to Order BDD Variables in Verification. |
J. Artif. Intell. Res. (JAIR) |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Doron Bustan, Orna Grumberg |
Simulation-based minimazation. |
ACM Trans. Comput. Log. |
2003 |
DBLP DOI BibTeX RDF |
Simulation, Minimization |
| 1 | Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster |
Scalable distributed on-the-fly symbolic model checking. |
STTT |
2003 |
DBLP DOI BibTeX RDF |
Distributed, Memory, BDDs, Counterexample |
| 1 | Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang |
High Level Verification of Control Intensive Systems Using Predicate Abstraction. |
MEMOCODE |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Tamir Heyman, Assaf Schuster |
A Work-Efficient Distributed Algorithm for Reachability Analysis. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang |
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi |
Enhanced Vacuity Detection in Linear Temporal Logic. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Shoham, Orna Grumberg |
A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Karen Yorav, Orna Grumberg |
Syntax-directed model checking of sequential programs. |
J. Log. Algebr. Program. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg |
Different directions in parallel and distributed model checking (invited talk). |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Lubos Brim, Orna Grumberg |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster |
A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits. |
Formal Methods in System Design |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Doron Bustan, Orna Grumberg |
Applicability of Fair Simulation. |
TACAS |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Katerina Korenblat, Orna Grumberg, Shmuel Katz |
Translations between Textual Transition Systems and Petri Nets. |
IFM |
2002 |
DBLP DOI BibTeX RDF |
textual transition systems, structure and semantics preservation, Petri nets, model translations |
| 1 | Shmuel Katz, Orna Grumberg |
A Framework for Translating Models and Specifications. |
IFM |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Sharon Barner, Orna Grumberg |
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Robert P. Kurshan |
Which Branching-Time Properties are Effectively Linear? |
J. Log. Comput. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg |
Introduction: Special Issue on CAV '97. |
Formal Methods in System Design |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Doron Peled |
Model checking. |
|
2001 |
RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith |
Progress on the State Explosion Problem in Model Checking. |
Informatics |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Tamir Heyman, Assaf Schuster |
Distributed Symbolic Model Checking for µ-Calculus. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Doron Bustan, Orna Grumberg |
Simulation Based Minimization. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster |
Scalable Distributed On-the-Fly Symbolic Model Checking. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster |
Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith |
Counterexample-Guided Abstraction Refinement. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Orna Grumberg |
Preface. |
Electr. Notes Theor. Comput. Sci. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Marius Minea, Doron Peled |
State Space Reduction Using Partial Order Techniques. |
STTT |
1999 |
DBLP DOI BibTeX RDF |
Partial order reduction, State space reduction |
| 1 | Sagi Katz, Orna Grumberg, Daniel Geist |
"Have I written enough Properties?" - A Method of Comparison between Specification and Implementation. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Karen Laster, Orna Grumberg |
Modular Model Checking of Software. |
TACAS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Jürgen Bohn, Werner Damm, Orna Grumberg, Hardi Hungar, Karen Laster |
First-Order-CTL Model Checking. |
FSTTCS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Somesh Jha |
Verifying Parameterized Networks. |
ACM Trans. Program. Lang. Syst. |
1997 |
DBLP DOI BibTeX RDF |
process invariants, model checking, temporal logic, parameterized systems |
| 1 | Dennis Dams, Rob Gerth, Orna Grumberg |
Abstract Interpretation of Reactive Systems. |
ACM Trans. Program. Lang. Syst. |
1997 |
DBLP DOI BibTeX RDF |
model checking, formal methods, abstract interpretation, reactive systems, mu-calculus |
| 1 | Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi |
Another Look at LTL Model Checking. |
Formal Methods in System Design |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg (eds.) |
Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings |
CAV |
1997 |
DBLP BibTeX RDF |
|
| 1 | Orna Kupferman, Orna Grumberg |
Branching-Time Temporal Logic and Tree Automata. |
Inf. Comput. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Limor Fix, Orna Grumberg |
Verification of Temporal Properties. |
J. Log. Comput. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Kupferman, Orna Grumberg |
Buy One, Get One Free!!! |
J. Log. Comput. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, David E. Long |
Model checking. |
NATO ASI DPD |
1996 |
DBLP BibTeX RDF |
|
| 1 | Sérgio Vale Aguiar Campos, Orna Grumberg |
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Somesh Jha |
Veryfying Parameterized Networks using Abstraction and Regular Languages. |
CONCUR |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao |
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. |
DAC |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Hardi Hungar, Orna Grumberg, Werner Damm |
What if model checking must be truly symbolic. |
CHARME |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Girish Bhat, Rance Cleaveland, Orna Grumberg |
Efficient On-the-Fly Model Checking for CTL* |
LICS |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Limor Fix, Nissim Francez, Orna Grumberg |
Program Composition via Unification. |
Theor. Comput. Sci. |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, David E. Long |
Model Checking and Abstraction. |
ACM Trans. Program. Lang. Syst. |
1994 |
DBLP DOI BibTeX RDF |
model checking, temporal logic, abstract interpretation, binary decision diagrams (BDDs) |
| 1 | Orna Grumberg, David E. Long |
Model Checking and Modular Verification. |
ACM Trans. Program. Lang. Syst. |
1994 |
DBLP DOI BibTeX RDF |
Moore machines, model checking, formal verification, temporal logics, CTL, computer-aided verification |
| 1 | Orna Bernholtz, Orna Grumberg |
Buy One, Get One Free!!! |
ICTL |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Robert P. Kurshan |
How Linear Can Branching-Time Be? |
ICTL |
1994 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")