Person: Orna Grumberg

DBLP: Grumberg:Orna

Facilitated 2 volumes:

Ed

Ed

Contributed to:

2015

2014

2013

2013

2012

2010

2008

2008

2007

2006

2006

2005

2005

2005

2005

2004

2003

2002

2002

2002

2001

2000

2000

1998

1996

1995

1995

1994

1993

1992

1992

1992

1991

1990

1990

1987

2016

Wrote 42 papers:

FM-2015-ElkaderGPS #automation #reasoning

Automated Circular Assume-Guarantee Reasoning (KAE, OG, CSP, SS), pp. 23–39.

IFM-2014-MellerGY #behaviour #uml #verification

Verifying Behavioral UML Systems via CEGAR (YM, OG, KY), pp. 139–154.

CAV-2013-SosnovichGN #network #protocol #security #using

Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems (AS, OG, GN), pp. 724–739.

TACAS-2013-VizelGS #analysis #reachability #using

Intertwined Forward-Backward Reachability Analysis Using Interpolants (YV, OG, SS), pp. 308–323.

FM-2012-GrumbergMY #behaviour #model checking #modelling #uml

Applying Software Model Checking Techniques for Behavioral UML Models (OG, YM, KY), pp. 277–292.

LATA-2010-GrumbergKS #automaton #infinity

Variable Automata over Infinite Alphabets (OG, OK, SS), pp. 561–572.

CAV-2008-JainCG #composition #equation #linear #performance

Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations (HJ, EMC, OG), pp. 254–267.

TACAS-2008-ChocklerGY #automation #performance #refinement #using

Efficient Automatic STE Refinement Using Responsibility (HC, OG, AY), pp. 233–248.

SAS-2007-ShohamG #abstraction #composition #verification

Compositional Verification and 3-Valued Abstractions Join Forces (SS, OG), pp. 69–86.

CAV-2006-TzorefG #automation #detection #evaluation #refinement

Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation (RT, OG), pp. 190–204.

LICS-2006-ShohamG #abstraction #precise

3-Valued Abstraction: More Precision at Less Cost (SS, OG), pp. 399–410.

CAV-2005-RabinovitzG #bound #concurrent #model checking #source code

Bounded Model Checking of Concurrent Programs (IR, OG), pp. 82–97.

IFM-2005-ChakiCGOSTV #specification #verification

State/Event Software Verification for Branching-Time Specifications (SC, EMC, OG, JO, NS, TT, HV), pp. 53–69.

POPL-2005-GrumbergLST #approximate #multi

Proof-guided underapproximation-widening for multi-process systems (OG, FL, OS, MT), pp. 122–131.

VMCAI-2005-GrumbergLLS #calculus

Don’t Know in the µ-Calculus (OG, ML, ML, SS), pp. 233–249.

TACAS-2004-ShohamG #abstraction

Monotonic Abstraction-Refinement for CTL (SS, OG), pp. 546–560.

CAV-2003-ArmoniFFGPTV #detection #linear #logic

Enhanced Vacuity Detection in Linear Temporal Logic (RA, LF, AF, OG, NP, AT, MYV), pp. 368–380.

CAV-2003-ClarkeGTW #abstraction #how #performance

Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates (EMC, OG, MT, DW), pp. 126–140.

CAV-2003-GrumbergHS #algorithm #analysis #distributed #reachability

A Work-Efficient Distributed Algorithm for Reachability Analysis (OG, TH, AS), pp. 54–66.

CAV-2003-ShohamG #abstraction #framework #game studies

A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement (SS, OG), pp. 275–287.

CAV-2002-BarnerG #approximate #model checking #reduction #symmetry

Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking (SB, OG), pp. 93–106.

IFM-2002-KatzG #framework #modelling #specification

A Framework for Translating Models and Specifications (SK, OG), pp. 145–164.

IFM-2002-KorenblatGK #petri net

Translations between Textual Transition Systems and Petri Nets (KK, OG, SK), pp. 339–359.

TACAS-2002-BustanG #simulation

Applicability of Fair Simulation (DB, OG), pp. 401–414.

CAV-2001-GrumbergHS #calculus #distributed #model checking #μ-calculus

Distributed Symbolic Model Checking for μ-Calculus (OG, TH, AS), pp. 350–362.

CADE-2000-BustanG #simulation

Simulation Based Minimization (DB, OG), pp. 255–270.

CAV-2000-ClarkeGJLV #abstraction #refinement

Counterexample-Guided Abstraction Refinement (EMC, OG, SJ, YL, HV), pp. 154–169.

CAV-2000-HeymanGGS #analysis #parallel #reachability #scalability

Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits (TH, DG, OG, AS), pp. 20–35.

TACAS-1998-LasterG #composition #model checking

Modular Model Checking of Software (KL, OG), pp. 20–35.

CAV-1996-CamposG #analysis #model checking #verification

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System (SVAC, OG), pp. 257–268.

DAC-1995-ClarkeGMZ #generative #model checking #performance

Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking (EMC, OG, KLM, XZ), pp. 427–432.

LICS-1995-BhatCG #model checking #on the fly #performance

Efficient On-the-Fly Model Checking for CTL* (GB, RC, OG), pp. 388–397.

CAV-1994-ClarkeGH #ltl #model checking

Another Look at LTL Model Checking (EMC, OG, KH), pp. 415–427.

CAV-1993-DamsGG #generative #modelling

Generation of Reduced Models for Checking Fragments of CTL (DD, OG, RG), pp. 479–490.

CAV-1992-De-LeonG #abstraction #composition #distributed #realtime #verification

Modular Abstractions for Verifying Real-Time Distributed Systems (HDL, OG), pp. 2–15.

ICALP-1992-FixFG #composition #unification

Program Composition via Unification (LF, NF, OG), pp. 672–684.

POPL-1992-ClarkeGL #abstraction #model checking

Model Checking and Abstraction (EMC, OG, DEL), pp. 342–354.

ICALP-1991-FixFG #composition #verification

Program Composition and Modular Verification (LF, NF, OG), pp. 93–114.

CAV-1990-ShurekG #composition #framework #verification

The Modular Framework of Computer-Aided Verification (GS, OG), pp. 214–223.

POPL-1990-AttieFG #interactive #multi

Fairness and Hyperfairness in Multi-Party Interactions (PCA, NF, OG), pp. 292–305.

CAAP-1987-BrowneCG #logic

Characterizing Kripke Structures in Temporal Logic (MCB, EMC, OG), pp. 256–270.

CAV-2016-ElkaderGPS #automation #composition #reasoning #refinement

Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement (KAE, OG, CSP, SS), pp. 329–351.