default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDOrna Grumberg
ארנה גרימברג
Person information
- affiliation: Technion - Israel Institute of Technology, Haifa, Israel
- unicode name: ארנה גרימברג
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[i6]Mishel Carelli, Orna Grumberg:
CTL* Verification and Synthesis using Existential Horn Clauses. CoRR abs/2408.11502 (2024)- 2023
- [c101]Omer Rappoport
, Orna Grumberg, Yakir Vizel:
Structure-Guided Solution of Constrained Horn Clauses. ATVA 2023: 117-138 - [c100]Bat-Chen Rothenberg, Orna Grumberg, Yakir Vizel, Eytan Singher:
Condition Synthesis Realizability via Constrained Horn Clauses. NFM 2023: 380-396 - 2022
- [j52]Sicun Gao, Orna Grumberg, Paolo Zuliani:
Edmund Melson Clarke, Jr. (1945-2020). Formal Methods Syst. Des. 60(3): 327-328 (2022) - [j51]Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald:
Assume, guarantee or repair: a regular framework for non regular properties. Int. J. Softw. Tools Technol. Transf. 24(5): 667-689 (2022) - [c99]Hadar Frenkel, Orna Grumberg, Bat-Chen Rothenberg, Sarai Sheinvald:
Automated Program Repair Using Formal Verification Techniques. Principles of Systems Design 2022: 511-534 - [i5]Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald:
Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties (full version). CoRR abs/2207.10534 (2022) - 2021
- [c98]Ohad Goudsmid, Orna Grumberg, Sarai Sheinvald:
Compositional Model Checking for Multi-properties. VMCAI 2021: 55-80 - [i4]Dan Rasin, Orna Grumberg, Sharon Shoham:
Modular Verification of Concurrent Programs via Sequential Model Checking. CoRR abs/2106.00732 (2021) - 2020
- [c97]Bat-Chen Rothenberg, Orna Grumberg:
Must Fault Localization for Program Repair. CAV (2) 2020: 658-680 - [c96]Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald:
Assume, Guarantee or Repair. TACAS (1) 2020: 211-227
2010 – 2019
- 2019
- [j50]Hadar Frenkel, Orna Grumberg, Sarai Sheinvald:
An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains. J. Autom. Reason. 63(4): 1077-1101 (2019) - [c95]Nurit Devir, Orna Grumberg, Shaul Markovitch, Gabi Nakibly:
Topology-Agnostic Runtime Detection of OSPF Routing Attacks. CNS 2019: 277-285 - 2018
- [b2]Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, Helmut Veith:
Model checking, 2nd Edition. MIT Press 2018, ISBN 978-0-262-03883-6 - [j49]Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham:
Automated circular assume-guarantee reasoning. Formal Aspects Comput. 30(5): 571-595 (2018) - [c94]Dan Rasin, Orna Grumberg, Sharon Shoham:
Modular Verification of Concurrent Programs via Sequential Model Checking. ATVA 2018: 228-247 - [c93]Bat-Chen Rothenberg, Orna Grumberg:
Program repair that learns from mistakes. ICSE (Companion Volume) 2018: 218-219 - [p5]Dennis Dams, Orna Grumberg:
Abstraction and Abstraction Refinement. Handbook of Model Checking 2018: 385-419 - 2017
- [c92]Hadar Frenkel, Orna Grumberg, Sarai Sheinvald:
An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data. NFM 2017: 1-18 - [c91]Anna Trostanetski, Orna Grumberg, Daniel Kroening:
Modular Demand-Driven Analysis of Semantic Difference for Program Versions. SAS 2017: 405-427 - [i3]Adi Sosnovich, Orna Grumberg, Gabi Nakibly:
Formal Black-Box Analysis of Routing Protocol Implementations. CoRR abs/1709.08096 (2017) - 2016
- [j48]Yael Meller, Orna Grumberg, Sharon Shoham:
A framework for compositional verification of multi-valued systems via abstraction-refinement. Inf. Comput. 247: 169-202 (2016) - [c90]Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham:
Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. CAV (1) 2016: 329-351 - [c89]Bat-Chen Rothenberg, Orna Grumberg:
Sound and Complete Mutation-Based Program Repair. FM 2016: 593-611 - [p4]Orna Grumberg, Yael Meller:
Learning-Based Compositional Model Checking of Behavioral UML Systems. Dependable Software Systems Engineering 2016: 117-136 - [e12]Javier Esparza, Orna Grumberg, Salomon Sickert:
Dependable Software Systems Engineering. NATO Science for Peace and Security Series - D: Information and Communication Security 45, IOS Press 2016, ISBN 978-1-61499-626-2 [contents] - [i2]Julian Dolby, Orna Grumberg, Peter Müller, Omer Tripp:
Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201). Dagstuhl Reports 6(5): 56-71 (2016) - 2015
- [c88]Yael Meller, Orna Grumberg, Karen Yorav:
Learning-Based Compositional Model Checking of Behavioral UML Systems. FACS 2015: 275-293 - [c87]Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham:
Automated Circular Assume-Guarantee Reasoning. FM 2015: 23-39 - [c86]Adi Sosnovich, Orna Grumberg, Gabi Nakibly:
Analyzing Internet Routing Security Using Model Checking. LPAR 2015: 112-129 - 2014
- [c85]Orna Grumberg, Orna Kupferman, Sarai Sheinvald:
A Game-Theoretic Approach to Simulation of Data-Parameterized Systems. ATVA 2014: 348-363 - [c84]Yael Meller, Orna Grumberg, Karen Yorav:
Verifying Behavioral UML Systems via CEGAR. IFM 2014: 139-154 - [p3]Orna Grumberg, Sharon Shoham, Yakir Vizel:
SAT-based Model Checking: Interpolation, IC3, and Beyond. Software Systems Safety 2014: 17-41 - [e11]Orna Grumberg, Helmut Seidl, Maximilian Irlbeck:
Software Systems Safety. NATO Science for Peace and Security Series, D: Information and Communication Security 36, IOS Press 2014, ISBN 978-1-61499-384-1 [contents] - 2013
- [c83]Orna Grumberg, Orna Kupferman, Sarai Sheinvald:
An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. ATVA 2013: 397-411 - [c82]Adi Sosnovich, Orna Grumberg, Gabi Nakibly:
Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems. CAV 2013: 724-739 - [c81]Yakir Vizel, Orna Grumberg, Sharon Shoham:
Intertwined Forward-Backward Reachability Analysis Using Interpolants. TACAS 2013: 308-323 - 2012
- [j47]Orna Grumberg, Moshe Y. Vardi, Joseph Sifakis, Rajeev Alur:
2010 CAV award announcement. Formal Methods Syst. Des. 40(2): 117-120 (2012) - [j46]Sharon Shoham, Orna Grumberg:
Multi-valued model checking games. J. Comput. Syst. Sci. 78(2): 414-429 (2012) - [c80]Orna Grumberg, Orna Kupferman, Sarai Sheinvald:
Model Checking Systems and Specifications with Parameterized Atomic Propositions. ATVA 2012: 122-136 - [c79]Orna Grumberg, Yael Meller, Karen Yorav:
Applying Software Model Checking Techniques for Behavioral UML Models. FM 2012: 277-292 - [c78]Yakir Vizel, Orna Grumberg, Sharon Shoham:
Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD 2012: 173-181 - [p2]Orna Grumberg:
Model Checking: From BDDs to Interpolation. Software Safety and Security 2012: 64-84 - [e10]Tobias Nipkow, Orna Grumberg, Benedikt Hauptmann:
Software Safety and Security - Tools for Analysis and Verification. NATO Science for Peace and Security Series - D: Information and Communication Security 33, IOS Press 2012, ISBN 978-1-61499-027-7 [contents] - 2011
- [i1]Orna Grumberg, Shlomi Livne, Shaul Markovitch:
Learning to Order BDD Variables in Verification. CoRR abs/1107.0020 (2011) - 2010
- [j45]Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi:
2009 CAV award announcement. Formal Methods Syst. Des. 36(3): 195-197 (2010) - [j44]Sharon Shoham, Orna Grumberg:
Compositional verification and 3-valued abstractions join forces. Inf. Comput. 208(2): 178-202 (2010) - [c77]Orna Grumberg, Orna Kupferman, Sarai Sheinvald:
Variable Automata over Infinite Alphabets. LATA 2010: 561-572 - [p1]Orna Grumberg:
2-Valued and 3-Valued Abstraction-Refinement in Model Checking. Logics and Languages for Reliability and Security 2010: 105-128 - [e9]Javier Esparza, Bernd Spanfelner, Orna Grumberg:
Logics and Languages for Reliability and Security. NATO Science for Peace and Security Series - D: Information and Communication Security 25, IOS Press 2010, ISBN 978-1-60750-099-5 [contents]
2000 – 2009
- 2009
- [j43]Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi:
The 2008 CAV Award citation. Formal Methods Syst. Des. 35(1): 4-5 (2009) - [j42]Himanshu Jain, Edmund M. Clarke, Orna Grumberg:
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Formal Methods Syst. Des. 35(1): 6-39 (2009) - [j41]Michael Huth, Orna Grumberg:
Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification. Int. J. Softw. Tools Technol. Transf. 11(2): 85-94 (2009) - [c76]Orna Grumberg:
3-Valued Abstraction for (Bounded) Model Checking. ATVA 2009: 21 - [c75]Yael Meller, Orna Grumberg, Sharon Shoham:
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. ATVA 2009: 271-288 - [c74]Avi Yadgar, Orna Grumberg, Assaf Schuster:
Hybrid BDD and All-SAT Method for Model Checking. Languages: From Formal to Natural 2009: 228-244 - [c73]Yakir Vizel, Orna Grumberg:
Interpolation-sequence based model checking. FMCAD 2009: 1-8 - [e8]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. Lecture Notes in Computer Science 5533, Springer 2009, ISBN 978-3-642-01747-6 [contents] - 2008
- [j40]Sharon Shoham, Orna Grumberg:
3-Valued abstraction: More precision at less cost. Inf. Comput. 206(11): 1313-1333 (2008) - [c72]Himanshu Jain, Edmund M. Clarke, Orna Grumberg:
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. CAV 2008: 254-267 - [c71]Hana Chockler, Orna Grumberg, Avi Yadgar:
Efficient Automatic STE Refinement Using Responsibility. TACAS 2008: 233-248 - [e7]Orna Grumberg, Helmut Veith:
25 Years of Model Checking - History, Achievements, Perspectives. Lecture Notes in Computer Science 5000, Springer 2008, ISBN 978-3-540-69849-4 [contents] - 2007
- [j39]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) - [j38]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) - [j37]Orna Grumberg, Shmuel Katz:
VeriTech: a framework for translating among model description notations. Int. J. Softw. Tools Technol. Transf. 9(2): 119-132 (2007) - [j36]Sharon Shoham, Orna Grumberg:
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Log. 9(1): 1 (2007) - [c70]Rotem Oshman, Orna Grumberg:
A New Approach to Bounded Model Checking for Branching Time Logics. ATVA 2007: 410-424 - [c69]Orna Grumberg, Assaf Schuster, Avi Yadgar:
3-Valued Circuit SAT for STE with Automatic Refinement. ATVA 2007: 457-473 - [c68]Sharon Shoham, Orna Grumberg:
Compositional Verification and 3-Valued Abstractions Join Forces. SAS 2007: 69-86 - [e6]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. Lecture Notes in Computer Science 4424, Springer 2007, ISBN 978-3-540-71208-4 [contents] - 2006
- [j35]Orna Grumberg, Tamir Heyman, Assaf Schuster:
A work-efficient distributed algorithm for reachability analysis. Formal Methods Syst. Des. 29(2): 157-175 (2006) - [c67]Rachel Tzoref, Orna Grumberg:
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation. CAV 2006: 190-204 - [c66]Sharon Shoham, Orna Grumberg:
3-Valued Abstraction: More Precision at Less Cost. LICS 2006: 399-410 - 2005
- [j34]Orna Grumberg, Tamir Heyman, Assaf Schuster:
Distributed Symbolic Model Checking for µ-Calculus. Formal Methods Syst. Des. 26(2): 197-219 (2005) - [j33]Sharon Barner, Orna Grumberg:
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. Formal Methods Syst. Des. 27(1-2): 29-66 (2005) - [j32]Lubos Brim, Orna Grumberg:
Introductory paper. Int. J. Softw. Tools Technol. Transf. 7(1): 1-3 (2005) - [c65]Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, Assaf Schuster:
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond. ATVA 2005: 11-25 - [c64]Sharon Shoham, Orna Grumberg:
Multi-valued Model Checking Games. ATVA 2005: 354-369 - [c63]Ishai Rabinovitz, Orna Grumberg:
Bounded Model Checking of Concurrent Programs. CAV 2005: 82-97 - [c62]Orna Grumberg, Tamir Heyman, Nili Ifergan, Assaf Schuster:
Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation. CHARME 2005: 129-145 - [c61]Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi:
Regular Vacuity. CHARME 2005: 191-206 - [c60]Orna Grumberg:
Abstraction and Refinement in Model Checking. FMCO 2005: 219-242 - [c59]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 - [c58]Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald:
Proof-guided underapproximation-widening for multi-process systems. POPL 2005: 122-131 - [c57]Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham:
Don't Know in the µ-Calculus. VMCAI 2005: 233-249 - 2004
- [j31]Karen Yorav, Orna Grumberg:
Static Analysis for State-Space Reductions Preserving Temporal Logics. Formal Methods Syst. Des. 25(1): 67-96 (2004) - [j30]Doron Bustan, Orna Grumberg:
Applicability of fair simulation. Inf. Comput. 194(1): 1-18 (2004) - [j29]Sérgio Vale Aguiar Campos, Orna Grumberg, Karen Yorav, Fady Copty:
Test sequence generation and model checking using dynamic transition relations. Int. J. Softw. Tools Technol. Transf. 6(2): 174-182 (2004) - [c56]Orna Grumberg, Assaf Schuster, Avi Yadgar:
Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis. FMCAD 2004: 275-289 - [c55]Sharon Shoham, Orna Grumberg:
Monotonic Abstraction-Refinement for CTL. TACAS 2004: 546-560 - 2003
- [j28]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) - [j27]Orna Grumberg, Shlomi Livne, Shaul Markovitch:
Learning to Order BDD Variables in Verification. J. Artif. Intell. Res. 18: 83-116 (2003) - [j26]Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster:
Scalable distributed on-the-fly symbolic model checking. Int. J. Softw. Tools Technol. Transf. 4(4): 496-504 (2003) - [j25]Doron Bustan, Orna Grumberg:
Simulation-based minimazation. ACM Trans. Comput. Log. 4(2): 181-206 (2003) - [c54]Orna Grumberg, Tamir Heyman, Assaf Schuster:
A Work-Efficient Distributed Algorithm for Reachability Analysis. CAV 2003: 54-66 - [c53]Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang:
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. CAV 2003: 126-140 - [c52]Sharon Shoham, Orna Grumberg:
A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. CAV 2003: 275-287 - [c51]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 - [c50]Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang:
High Level Verification of Control Intensive Systems Using Predicate Abstraction. MEMOCODE 2003: 55-64 - [c49]Lubos Brim, Orna Grumberg:
Preface. PDMC@CAV 2003: 1-2 - [e5]Lubos Brim, Orna Grumberg:
2nd International Workshop on Parallel and Distributed Model Checking, PDMC 2003, Satellite Workshop of CAV 2003, Boulder, Colorado, USA, July 13, 2003. Electronic Notes in Theoretical Computer Science 89(1), Elsevier 2003 [contents] - [e4]Lubos Brim, Orna Grumberg:
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. Electronic Notes in Theoretical Computer Science 86(3), Elsevier 2003 [contents] - 2002
- [j24]Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster:
A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits. Formal Methods Syst. Des. 21(3): 317-338 (2002) - [j23]Karen Yorav, Orna Grumberg:
Syntax-directed model checking of sequential programs. J. Log. Algebraic Methods Program. 52-53: 129-162 (2002) - [c48]Sharon Barner, Orna Grumberg:
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. CAV 2002: 93-106 - [c47]Shmuel Katz, Orna Grumberg:
A Framework for Translating Models and Specifications. IFM 2002: 145-164 - [c46]Katerina Korenblat, Orna Grumberg, Shmuel Katz:
Translations between Textual Transition Systems and Petri Nets. IFM 2002: 339-359 - [c45]Doron Bustan, Orna Grumberg:
Applicability of Fair Simulation. TACAS 2002: 401-414 - [c44]Lubos Brim, Orna Grumberg:
Preface. PDMC@CONCUR 2002: 483 - [c43]Orna Grumberg:
Different directions in parallel and distributed model checking (invited talk). PDMC@CONCUR 2002: 485 - [e3]Lubos Brim, Orna Grumberg:
Parallel and Distributed Model Checking, PDMC 2002, Satellite Workshop of CONCUR 2002, Brno, Czech Republic, August 19, 2002. Electronic Notes in Theoretical Computer Science 68(4), Elsevier 2002 [contents] - 2001
- [b1]Edmund M. Clarke, Orna Grumberg, Doron A. Peled:
Model checking, 1st Edition. MIT Press 2001, ISBN 978-0-262-03270-4, pp. I-XIV, 1-314 - [j22]Orna Grumberg:
Introduction: Special Issue on CAV '97. Formal Methods Syst. Des. 18(2): 95 (2001) - [j21]Orna Grumberg, Robert P. Kurshan:
Which Branching-Time Properties are Effectively Linear? J. Log. Comput. 11(2): 201-228 (2001) - [c42]Orna Grumberg, Tamir Heyman, Assaf Schuster:
Distributed Symbolic Model Checking for µ-Calculus. CAV 2001: 350-362 - [c41]Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith:
Progress on the State Explosion Problem in Model Checking. Informatics 2001: 176-194 - 2000
- [j20]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 Syst. Des. 17(2): 163-192 (2000) - [c40]Doron Bustan, Orna Grumberg:
Simulation Based Minimization. CADE 2000: 255-270 - [c39]Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster:
Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. CAV 2000: 20-35 - [c38]Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu,