 | 2009 |
|---|
| 118 |       | Orna Grumberg,
Michael Kaminski,
Shmuel Katz,
Shuly Wintner:
Languages: From Formal to Natural, Essays Dedicated to Nissim Francez on the Occasion of His 65th Birthday
Springer 2009 |
| 117 | | Orna Grumberg:
3-Valued Abstraction for (Bounded) Model Checking.
ATVA 2009: 21 |
| 116 | | Yael Meller,
Orna Grumberg,
Sharon Shoham:
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement.
ATVA 2009: 271-288 |
| 115 | | Avi Yadgar,
Orna Grumberg,
Assaf Schuster:
Hybrid BDD and All-SAT Method for Model Checking.
Languages: From Formal to Natural 2009: 228-244 |
| 114 | | 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) |
| 2008 |
|---|
| 113 |  | Orna Grumberg,
Helmut Veith:
25 Years of Model Checking - History, Achievements, Perspectives
Springer 2008 |
| 112 | | Himanshu Jain,
Edmund M. Clarke,
Orna Grumberg:
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations.
CAV 2008: 254-267 |
| 111 | | Hana Chockler,
Orna Grumberg,
Avi Yadgar:
Efficient Automatic STE Refinement Using Responsibility.
TACAS 2008: 233-248 |
| 110 | | Sharon Shoham,
Orna Grumberg:
3-Valued abstraction: More precision at less cost.
Inf. Comput. 206(11): 1313-1333 (2008) |
| 2007 |
|---|
| 109 | | Orna Grumberg,
Michael Huth:
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
Springer 2007 |
| 108 | | Rotem Oshman,
Orna Grumberg:
A New Approach to Bounded Model Checking for Branching Time Logics.
ATVA 2007: 410-424 |
| 107 | | Orna Grumberg,
Assaf Schuster,
Avi Yadgar:
3-Valued Circuit SAT for STE with Automatic Refinement.
ATVA 2007: 457-473 |
| 106 | | Sharon Shoham,
Orna Grumberg:
Compositional Verification and 3-Valued Abstractions Join Forces.
SAS 2007: 69-86 |
| 105 | | Sharon Shoham,
Orna Grumberg:
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
ACM Trans. Comput. Log. 9(1): (2007) |
| 104 | | 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) |
| 103 | | 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) |
| 102 | | Orna Grumberg,
Shmuel Katz:
VeriTech: a framework for translating among model description notations.
STTT 9(2): 119-132 (2007) |
| 2006 |
|---|
| 101 | | Rachel Tzoref,
Orna Grumberg:
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation.
CAV 2006: 190-204 |
| 100 | | Sharon Shoham,
Orna Grumberg:
3-Valued Abstraction: More Precision at Less Cost.
LICS 2006: 399-410 |
| 99 | | Orna Grumberg,
Tamir Heyman,
Assaf Schuster:
A work-efficient distributed algorithm for reachability analysis.
Formal Methods in System Design 29(2): 157-175 (2006) |
| 2005 |
|---|
| 98 | | Limor Fix,
Orna Grumberg,
Amnon Heyman,
Tamir Heyman,
Assaf Schuster:
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond.
ATVA 2005: 11-25 |
| 97 | | Sharon Shoham,
Orna Grumberg:
Multi-valued Model Checking Games.
ATVA 2005: 354-369 |
| 96 | | Ishai Rabinovitz,
Orna Grumberg:
Bounded Model Checking of Concurrent Programs.
CAV 2005: 82-97 |
| 95 | | Orna Grumberg,
Tamir Heyman,
Nili Ifergan,
Assaf Schuster:
Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation.
CHARME 2005: 129-145 |
| 94 | | Doron Bustan,
Alon Flaisher,
Orna Grumberg,
Orna Kupferman,
Moshe Y. Vardi:
Regular Vacuity.
CHARME 2005: 191-206 |
| 93 | | Orna Grumberg:
Abstraction and Refinement in Model Checking.
FMCO 2005: 219-242 |
| 92 | | 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 |
| 91 | | Orna Grumberg,
Flavio Lerda,
Ofer Strichman,
Michael Theobald:
Proof-guided underapproximation-widening for multi-process systems.
POPL 2005: 122-131 |
| 90 | | Orna Grumberg,
Martin Lange,
Martin Leucker,
Sharon Shoham:
Don't Know in the µ-Calculus.
VMCAI 2005: 233-249 |
| 89 | | Orna Grumberg,
Tamir Heyman,
Assaf Schuster:
Distributed Symbolic Model Checking for µ-Calculus.
Formal Methods in System Design 26(2): 197-219 (2005) |
| 88 | | 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) |
| 87 | | Lubos Brim,
Orna Grumberg:
Introductory paper.
STTT 7(1): 1-3 (2005) |
| 2004 |
|---|
| 86 | | Orna Grumberg,
Assaf Schuster,
Avi Yadgar:
Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis.
FMCAD 2004: 275-289 |
| 85 | | Sharon Shoham,
Orna Grumberg:
Monotonic Abstraction-Refinement for CTL.
TACAS 2004: 546-560 |
| 84 | | Karen Yorav,
Orna Grumberg:
Static Analysis for State-Space Reductions Preserving Temporal Logics.
Formal Methods in System Design 25(1): 67-96 (2004) |
| 83 | | Doron Bustan,
Orna Grumberg:
Applicability of fair simulation.
Inf. Comput. 194(1): 1-18 (2004) |
| 82 | | 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) |
| 2003 |
|---|
| 81 | | Edmund M. Clarke,
Orna Grumberg,
Muralidhar Talupur,
Dong Wang:
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates.
CAV 2003: 126-140 |
| 80 | | Sharon Shoham,
Orna Grumberg:
A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement.
CAV 2003: 275-287 |
| 79 | | 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 |
| 78 | | Orna Grumberg,
Tamir Heyman,
Assaf Schuster:
A Work-Efficient Distributed Algorithm for Reachability Analysis.
CAV 2003: 54-66 |
| 77 | | Edmund M. Clarke,
Orna Grumberg,
Muralidhar Talupur,
Dong Wang:
High Level Verification of Control Intensive Systems Using Predicate Abstraction.
MEMOCODE 2003: 55-64 |
| 76 | | Doron Bustan,
Orna Grumberg:
Simulation-based minimazation.
ACM Trans. Comput. Log. 4(2): 181-206 (2003) |
| 75 | | Lubos Brim,
Orna Grumberg:
Preface.
Electr. Notes Theor. Comput. Sci. 89(1): (2003) |
| 74 | | 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) |
| 73 | | Orna Grumberg,
Shlomi Livne,
Shaul Markovitch:
Learning to Order BDD Variables in Verification.
J. Artif. Intell. Res. (JAIR) 18: 83-116 (2003) |
| 72 | | Shoham Ben-David,
Orna Grumberg,
Tamir Heyman,
Assaf Schuster:
Scalable distributed on-the-fly symbolic model checking.
STTT 4(4): 496-504 (2003) |
| 2002 |
|---|
| 71 | | Sharon Barner,
Orna Grumberg:
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking.
CAV 2002: 93-106 |
| 70 | | Shmuel Katz,
Orna Grumberg:
A Framework for Translating Models and Specifications.
IFM 2002: 145-164 |
| 69 | | Katerina Korenblat,
Orna Grumberg,
Shmuel Katz:
Translations between Textual Transition Systems and Petri Nets.
IFM 2002: 339-359 |
| 68 | | Doron Bustan,
Orna Grumberg:
Applicability of Fair Simulation.
TACAS 2002: 401-414 |
| 67 | | Orna Grumberg:
Different directions in parallel and distributed model checking (invited talk).
Electr. Notes Theor. Comput. Sci. 68(4): (2002) |
| 66 | | Lubos Brim,
Orna Grumberg:
Preface.
Electr. Notes Theor. Comput. Sci. 68(4): (2002) |
| 65 | | 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) |
| 64 | | Karen Yorav,
Orna Grumberg:
Syntax-directed model checking of sequential programs.
J. Log. Algebr. Program. 52-53: 129-162 (2002) |
| 2001 |
|---|
| 63 | | Orna Grumberg,
Tamir Heyman,
Assaf Schuster:
Distributed Symbolic Model Checking for µ-Calculus.
CAV 2001: 350-362 |
| 62 | | Edmund M. Clarke,
Orna Grumberg,
Somesh Jha,
Yuan Lu,
Helmut Veith:
Progress on the State Explosion Problem in Model Checking.
Informatics 2001: 176-194 |
| 61 | | Orna Grumberg:
Introduction: Special Issue on CAV '97.
Formal Methods in System Design 18(2): 95 (2001) |
| 60 | | Orna Grumberg,
Robert P. Kurshan:
Which Branching-Time Properties are Effectively Linear?
J. Log. Comput. 11(2): 201-228 (2001) |
| 2000 |
|---|
| 59 | | Doron Bustan,
Orna Grumberg:
Simulation Based Minimization.
CADE 2000: 255-270 |
| 58 | | Edmund M. Clarke,
Orna Grumberg,
Somesh Jha,
Yuan Lu,
Helmut Veith:
Counterexample-Guided Abstraction Refinement.
CAV 2000: 154-169 |
| 57 | | Tamir Heyman,
Daniel Geist,
Orna Grumberg,
Assaf Schuster:
Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits.
CAV 2000: 20-35 |
| 56 | | Shoham Ben-David,
Tamir Heyman,
Orna Grumberg,
Assaf Schuster:
Scalable Distributed On-the-Fly Symbolic Model Checking.
FMCAD 2000: 390-404 |
| 55 | | 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) |
| 1999 |
|---|
| 54 | | Sagi Katz,
Orna Grumberg,
Daniel Geist:
"Have I written enough Properties?" - A Method of Comparison between Specification and Implementation.
CHARME 1999: 280-297 |
| 53 | | Alessandro Cimatti,
Orna Grumberg:
Preface.
Electr. Notes Theor. Comput. Sci. 23(2): (1999) |
| 52 | | Edmund M. Clarke,
Orna Grumberg,
Marius Minea,
Doron Peled:
State Space Reduction Using Partial Order Techniques.
STTT 2(3): 279-287 (1999) |
| 1998 |
|---|
| 51 | | Jürgen Bohn,
Werner Damm,
Orna Grumberg,
Hardi Hungar,
Karen Laster:
First-Order-CTL Model Checking.
FSTTCS 1998: 283-294 |
| 50 | | Karen Laster,
Orna Grumberg:
Modular Model Checking of Software.
TACAS 1998: 20-35 |
| 1997 |
|---|
| 49 | | Orna Grumberg:
Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings
Springer 1997 |
| 48 | | Dennis Dams,
Rob Gerth,
Orna Grumberg:
Abstract Interpretation of Reactive Systems.
ACM Trans. Program. Lang. Syst. 19(2): 253-291 (1997) |
| 47 | | Edmund M. Clarke,
Orna Grumberg,
Somesh Jha:
Verifying Parameterized Networks.
ACM Trans. Program. Lang. Syst. 19(5): 726-750 (1997) |
| 46 | | Edmund M. Clarke,
Orna Grumberg,
Kiyoharu Hamaguchi:
Another Look at LTL Model Checking.
Formal Methods in System Design 10(1): 47-71 (1997) |
| 1996 |
|---|
| 45 | | Sérgio Vale Aguiar Campos,
Orna Grumberg:
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System.
CAV 1996: 257-268 |
| 44 | | Edmund M. Clarke,
Orna Grumberg,
David E. Long:
Model checking.
NATO ASI DPD 1996: 305-349 |
| 43 | | Orna Kupferman,
Orna Grumberg:
Branching-Time Temporal Logic and Tree Automata.
Inf. Comput. 125(1): 62-69 (1996) |
| 42 | | Limor Fix,
Orna Grumberg:
Verification of Temporal Properties.
J. Log. Comput. 6(3): 343-361 (1996) |
| 41 | | Orna Kupferman,
Orna Grumberg:
Buy One, Get One Free!!!
J. Log. Comput. 6(4): 523-539 (1996) |
| 1995 |
|---|
| 40 | | Hardi Hungar,
Orna Grumberg,
Werner Damm:
What if model checking must be truly symbolic.
CHARME 1995: 1-20 |
| 39 | | Edmund M. Clarke,
Orna Grumberg,
Somesh Jha:
Veryfying Parameterized Networks using Abstraction and Regular Languages.
CONCUR 1995: 395-407 |
| 38 | | Edmund M. Clarke,
Orna Grumberg,
Kenneth L. McMillan,
Xudong Zhao:
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.
DAC 1995: 427-432 |
| 37 | | Girish Bhat,
Rance Cleaveland,
Orna Grumberg:
Efficient On-the-Fly Model Checking for CTL*
LICS 1995: 388-397 |
| 36 | | 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) |
| 1994 |
|---|
| 35 | | Edmund M. Clarke,
Orna Grumberg,
Kiyoharu Hamaguchi:
Another Look at LTL Model Checking.
CAV 1994: 415-427 |
| 34 | | Orna Grumberg,
Robert P. Kurshan:
How Linear Can Branching-Time Be?
ICTL 1994: 180-194 |
| 33 | | Orna Bernholtz,
Orna Grumberg:
Buy One, Get One Free!!!
ICTL 1994: 210-224 |
| 32 | | Orna Grumberg,
David E. Long:
Model Checking and Modular Verification.
ACM Trans. Program. Lang. Syst. 16(3): 843-871 (1994) |
| 31 | | Edmund M. Clarke,
Orna Grumberg,
David E. Long:
Model Checking and Abstraction.
ACM Trans. Program. Lang. Syst. 16(5): 1512-1542 (1994) |
| 30 | | Limor Fix,
Nissim Francez,
Orna Grumberg:
Program Composition via Unification.
Theor. Comput. Sci. 131(1): 139-179 (1994) |
| 1993 |
|---|
| 29 | | Dennis Dams,
Orna Grumberg,
Rob Gerth:
Generation of Reduced Models for Checking Fragments of CTL.
CAV 1993: 479-490 |
| 28 | | 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 |
| 27 | | Orna Bernholtz,
Orna Grumberg:
Branching Time Temporal Logic and Amorphous Tree Automata.
CONCUR 1993: 262-277 |
| 26 | | Edmund M. Clarke,
Orna Grumberg,
David E. Long:
Verification Tools for Finite-State Concurrent Systems.
REX School/Symposium 1993: 124-175 |
| 25 | | Paul C. Attie,
Nissim Francez,
Orna Grumberg:
Fairness and Hyperfairness in Multi-Party Interactions.
Distributed Computing 6(4): 245-254 (1993) |
| 24 | | Hana De-Leon,
Orna Grumberg:
Modular Abstractions for Verifying Real-Time Distributed Systems.
Formal Methods in System Design 2(1): 7-43 (1993) |
| 1992 |
|---|
| 23 | | Hana De-Leon,
Orna Grumberg:
Modular Abstractions for Verifying Real-Time Distributed Systems.
CAV 1992: 2-15 |
| 22 | | Limor Fix,
Nissim Francez,
Orna Grumberg:
Program Composition via Unification.
ICALP 1992: 672-684 |
| 21 | | Edmund M. Clarke,
Orna Grumberg,
David E. Long:
Model Checking and Abstraction.
POPL 1992: 342-354 |
| 20 | | 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) |
| 1991 |
|---|
| 19 | | Orna Grumberg,
David E. Long:
Model Checking and Modular Verification.
CONCUR 1991: 250-265 |
| 18 | | Limor Fix,
Nissim Francez,
Orna Grumberg:
Program Composition and Modular Verification.
ICALP 1991: 93-114 |
| 1990 |
|---|
| 17 | | Gil Shurek,
Orna Grumberg:
The Modular Framework of Computer-Aided Verification.
CAV 1990: 214-223 |
| 16 | | Paul C. Attie,
Nissim Francez,
Orna Grumberg:
Fairness and Hyperfairness in Multi-Party Interactions.
POPL 1990: 292-305 |
| 1989 |
|---|
| 15 | | Ze'ev Shtadler,
Orna Grumberg:
Network Grammars, Communication Behaviors and Automatic Verification.
Automatic Verification Methods for Finite State Systems 1989: 151-165 |
| 14 | | 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 |
| 13 | | Michael C. Browne,
Edmund M. Clarke,
Orna Grumberg:
Reasoning about Networks with Many Identical Finite State Processes
Inf. Comput. 81(1): 13-31 (1989) |
| 1988 |
|---|
| 12 | | Ran Rinat,
Nissim Francez,
Orna Grumberg:
Infinite Trees, Markings and Well-Foundedness
Inf. Comput. 79(2): 131-154 (1988) |
| 11 | | Michael C. Browne,
Edmund M. Clarke,
Orna Grumberg:
Characterizing Finite Kripke Structures in Propositional Temporal Logic.
Theor. Comput. Sci. 59: 115-131 (1988) |
| 1987 |
|---|
| 10 | | Edmund M. Clarke,
Orna Grumberg:
Avoiding The State Explosion Problem in Temporal Logic Model Checking.
PODC 1987: 294-303 |
| 9 | | Michael C. Browne,
Edmund M. Clarke,
Orna Grumberg:
Characterizing Kripke Structures in Temporal Logic.
TAPSOFT, Vol.1 1987: 256-270 |
| 8 | | Edmund M. Clarke,
Orna Grumberg:
The Model Checking Problem for Concurrent Systems with Many Similar Processes.
Temporal Logic in Specification 1987: 188-201 |
| 1986 |
|---|
| 7 | | Ran Rinat,
Nissim Francez,
Orna Grumberg:
Infinite Trees, Markings and Well Foundedness.
CAAP 1986: 238-253 |
| 6 | | Edmund M. Clarke,
Orna Grumberg,
Michael C. Browne:
Reasoning About Networks With Many Identical Finite-State Processes.
PODC 1986: 240-248 |
| 5 | | Orna Grumberg,
Nissim Francez,
Shmuel Katz:
A Complete Rule for Equifair Termination.
J. Comput. Syst. Sci. 33(3): 313-332 (1986) |
| 1985 |
|---|
| 4 | | Nissim Francez,
Orna Grumberg,
Shmuel Katz,
Amir Pnueli:
Proving Termination of Prolog Programs.
Logic of Programs 1985: 89-105 |
| 3 | | 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) |
| 1984 |
|---|
| 2 | | Orna Grumberg,
Nissim Francez,
Shmuel Katz:
Fail Termination of Communicating Processe.
PODC 1984: 254-265 |
| 1983 |
|---|
| 1 | | Orna Grumberg,
Nissim Francez,
Shmuel Katz:
A Compete Proof Rule for Strong Equifair Termination.
Logic of Programs 1983: 257-278 |
