BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Canada
1 × Finland
1 × Germany
1 × Greece
1 × Hungary
1 × Norway
1 × Portugal
1 × Russia
1 × The Netherlands
1 × United Kingdom
14 × USA
2 × Denmark
2 × Italy
2 × Spain
4 × France
Collaborated with:
S.Shoham E.M.Clarke D.Bustan N.Francez T.Heyman A.Schuster S.Katz L.Fix Y.Meller K.Yorav K.A.Elkader C.S.Pasareanu R.Tzoref I.Rabinovitz S.Barner K.Laster S.V.A.Campos H.De-Leon G.Shurek H.Veith A.Sosnovich G.Nakibly Y.Vizel O.Kupferman S.Sheinvald H.Jain H.Chockler A.Yadgar K.Korenblat G.Bhat R.Cleaveland K.Hamaguchi D.Dams R.Gerth D.E.Long P.C.Attie M.C.Browne F.Lerda O.Strichman M.Theobald M.Lange M.Leucker M.Talupur D.Wang D.Geist K.L.McMillan X.Zhao S.Jha Y.Lu S.Chaki J.Ouaknine N.Sharygina T.Touili R.Armoni A.Flaisher N.Piterman A.Tiemeyer M.Y.Vardi
Talks about:
model (13) check (11) abstract (8) system (6) effici (6) refin (6) modular (5) analysi (4) symbol (4) verif (4)

Person: Orna Grumberg

DBLP DBLP: Grumberg:Orna

Facilitated 2 volumes:

TACAS 2007Ed
CAV 1997Ed

Contributed to:

FM 20152015
IFM 20142014
CAV 20132013
TACAS 20132013
FM 20122012
LATA 20102010
CAV 20082008
TACAS 20082008
SAS 20072007
CAV 20062006
LICS 20062006
CAV 20052005
IFM 20052005
POPL 20052005
VMCAI 20052005
TACAS 20042004
CAV 20032003
CAV 20022002
IFM 20022002
TACAS 20022002
CAV 20012001
CADE 20002000
CAV 20002000
TACAS 19981998
CAV 19961996
DAC 19951995
LICS 19951995
CAV 19941994
CAV 19931993
CAV 19921992
ICALP 19921992
POPL 19921992
ICALP 19911991
CAV 19901990
POPL 19901990
TAPSOFT, Vol.1: CAAP 19871987
CAV (1) 20162016

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.