Publications - Orna Grumberg

Book

E.M.Clarke, O. Grumberg, D. Peled:
“Model Checking”, MIT Press, December 1999.
ISBN 0-262-03270-8
E.M.Clarke, O. Grumberg, D. Kroening, D. Peled, H. Veith:
“Model Checking, Second Edition”, MIT Press, December 2018.
ISBN 9780262038836

Publications related to static analysis, abstraction, and modularity in model checking
(Not updated and not exhaustive)

O.Grumberg, D.E.Long:
“Model Checking and Modular Verification“,
ACM-TOPLAS, Vol. 16, No. 3, 843–871 , May 1994.
E.M.Clarke, O.Grumberg, D.E.Long:
“Model Checking and Abstraction“,
ACM-TOPLAS, Vol. 16, No. 5, 1512- , September 1994.
D.Dams, R.Gerth, O.Grumberg:
“Abstract Interpretation of Reactive Systems“,
ACM Transactions on Programming Languages and Systems
(TOPLAS), Vol. 19, No. 2, March 1997.
K.Yorav, O.Grumberg:
“Static Analysis for State-Space Reductions Preserving Temporal
Logics“,
TR #CS-2000-03, Computer Science Department, Technion, Israel.
Formal Methods in Systems Design.
O. Grumberg:
“Abstractions and Reductions in Model Checking “,
in Nato Science Series, Vol. 62, 2001, Marktoberdorf summer school.
E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith,
“Counterexample-guided Abstraction Refinement“,
International Conference on Computer Aided Verification (CAV’00),
Chicago, July 2000.
S. Shoham, O. Grumberg:
“A Game-Based Framework for CTL Counter-Examples and 3-Valued
Abstraction-Refinement “,
International Conference on Computer Aided Verification (CAV’03),
Bolder, Colorado, July, 2003.
S. Shoham, O. Grumberg:
“Monotonic Abstraction-Refinement for CTL “,
Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’04), Barcelona, April 2004.
O. Grumberg, M. Lange, M. Leucker, S. Shoham:
“Don’t Know in Mu-Calculus“,
The 6th International Conference on
Verification, Model Checking, and Abstract Interpretation (VMCAI’05), Paris, January 2005.
S. Shoham, O. Grumberg:
“ 3-Valued Abstraction: More Precision at Less Cost “,
Twenty-first Annual IEEE Symposium on Logic in Computer Science (LICS’06), Seattle, Washington, August, 2006.
S. Shoham, O. Grumberg:
“Compositional Verification and 3-Valued Abstractions Join Forces “,
Static Analysis Symposium (SAS’07), Kongens Lyngby, Denmark,
August 2007.
Y. Meller, O. Grumberg, S. Shoham:
“A Framework for Compositional Verification of Multi-Valued Systems via Abstraction-Refinement “,
7th International Symposium on Automated Technology for Verification and Analysis (ATVA’09), Macao, October 2009.
Y. Meller, O. Grumberg, K. Yorav:
“Verifying Behavioral UML Systems via CEGAR”,
The 11th International Conference on Integrated Formal Methods (iFM 2014), Bertinoro, Italy,
September, 2014.
K. Abd Elkader, O. Grumberg, C.S. Pasareanu, S. Shoham:
“Automated Circular Assume-Guarantee Reasoning”,
20th International Symposium on Formal Methods (FM’15), Oslo, June 2015.
Y. Meller, O. Grumberg, K. Yorav:
“Learning-Based Compositional Model Checking of Behavioral UML Systems”,
International Conference on Formal aspects of Component Software (FACS’15), Rio de Janeiro, Brazil, October 2015.
K. Abd Elkader, O. Grumberg, C.S. Pasareanu, S. Shoham:
“Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement”,
Computer-Aided Verification (CAV’16), Toronto, July 2016.
Anna Trostanetski, Orna Grumberg, Daniel Kroening:
“Modular Demand-Driven Analysis of Semantic Difference for Program Versions”,
24th Static Analysis Symposium (SAS’17), New York City, NY, USA, August, 2017.

Surveys

E.M.Clarke, O. Grumberg, D.E. Long:
“Verification Tools for Finite-State Concurrent Systems“,
LNCS 803, in the proceedings of REX school/symposium on
A decade of concurrency: reflections and perspectives,
Noordwijkerhout, The Netherlands, June 1993.
E.M.Clarke, O. Grumberg, D.E. Long:
“Model Checking“,
in Springer-Verlag Nato ASI Series F, Volume 152, 1996,
Marktoberdorf summer school
(a survey on model checking, abstraction and composition).
O. Grumberg:
“Abstractions and Reductions in Model Checking “,
in Nato Science Series, Vol. 62, 2001, Marktoberdorf summer school.
S.Katz, O. Grumberg:
“A framework for translating models and specifications “,
Third international conference on Integrated Formal
Methods (IFM’02), Turku, Finland, May 2002.
O. Grumberg:
“Abstraction and Refinement in Model Checking “,
International Conference on Formal Methods for Components and Objects (FMCO 2005), Leiden, The Netherlands, November 2005.
O. Grumberg:
“Symbolic Trajectory Evaluation (STE):
Automatic Refinement and Vacuity Detection “,
in Nato Science Series, Volume 14, 2007.
O. Grumberg:
“2-Valued and 3-Valued Abstraction-Refinement in Model Checking “,
in Nato Science Series, Volume 25, 2009.
O. Grumberg:
“Model Checking: from BDDs to Interpolation “,
in Nato Science Series, Volume 33, 2011.
O. Grumberg, S. Shoham, Y. Vizel:
“SAT-based Model Checking: Interpolation, IC3, and Beyond “,
in Nato Science Series, Volume 36, 2013.
O. Grumberg, Y. Meller:
“Learning-Based Compositional Model Checking of Behavioral UML Systems”,
in Nato Science Series, volume 45, 2015.

Journals

O.Grumberg, N.Francez, J.A.Makowsky, W.P.deRoever:
“A proof rule for fair termination of guarded commands”,
Information and Control 66, 1/2: 83-102, July/August 1985.
O.Grumberg, N.Francez, S.Katz:
“A complete proof rule for equifair termination”,
JCSS 33, 3: 313-332, Dec. 1986.
E.M.Clarke, O.Grumberg:
“Research on automatic verification of finite-state concurrent systems”,
Annual Reviews of Computer Science, Vol. 2, 269-290, 1987 (J.F. Traub, editor).
M.C.Browne, E.M.Clarke, O.Grumberg:
“Characterizing finite Kripke structures in propositional temporal logic”,
Theoretical Computer Science 59, 115-131, 1988.
R.Rinat, N.Francez, O.Grumberg:
“Infinite trees, markings and well foundedness”,
Information and Computations 79, 131-154 (1988).
E.M.Clarke, O.Grumberg, M.C.Browne:
“Reasoning about networks with many identical finite-state processes”,
Information and Computations 81, 13-31 (1989).
E.M.Clarke, J.R.Burch, O.Grumberg, D.E.Long, K.L.McMillan:
“Automatic Verification of Sequential Circuit Designs”,
The Philosophical Transactions of the Royal Society, series A, 339, 105-120 (1992).
on Mechanized Reasoning and Hardware Design.
E.M.Clarke, O.Grumberg, R.P.Kurshan:
“A synthesis of two approaches for verifying finite state concurrent systems”,
Logic and Computation, Vol. 2 No. 5, 605-618 (1992).
H.De-Leon, O.Grumberg:
“Modular Abstractions for Verifying Real-Time Distributed Systems”,
Formal Methods in System Design, vol. 2, no. 1, February 1993.
P.Attie, N.Francez, O.Grumberg:
“Fairness and hyperfairness in multi-party interactions”,
Distributed Computing, Vol. 6, 245-254 (1993).
O.Grumberg, D.E.Long:
“Model Checking and Modular Verification“,
ACM-TOPLAS, Vol. 16, No. 3, 843–871 , May 1994.
L.Fix, N.Francez, O.Grumberg:
“Program Composition via Unification“,
Theoretical Computer Science, Vol. 131, 139-179 (1994).
E.M.Clarke, O.Grumberg, D.E.Long:
“Model Checking and Abstraction“,
ACM-TOPLAS, Vol. 16, No. 5, 1512- , September 1994.
E.M.Clarke, O.Grumberg, H.Hiraishi, S.Jha, D.E.Long, K.L.McMillan,
L.A.Ness:
“Verification of the Futurebus+ Cache Coherence Protocol“,
Formal Methods in System Design Vol. 6, No. 2, 217-232, March 1995.
L.Fix, O.Grumberg:
“Verification of Temporal Properties“,
Logic and Computation, Volume 6, number 3, pp 343–362, 1996.
O. Kupferman, O. Grumberg:
“Buy one, get one free!“,
Logic and Computation, Volume 6, number 4, 523-539, 1996.
O.Kupferman, O.Grumberg:
“Branching Time Temporal Logic and Amorphous Tree Automata“,
Information and Computation, 125(1):62-69, 25 February 1996.
E. Clarke, O. Grumberg, H. Hamaguchi:
“Another Look at LTL Model Checking“,
Formal Methods in System Design, Volume 10, Number 1,
February 1997. Also in CAV’94.
D.Dams, R.Gerth, O.Grumberg:
“Abstract Interpretation of Reactive Systems“,
ACM Transactions on Programming Languages and Systems
(TOPLAS), Vol. 19, No. 2, March 1997.
S. Campos, E.M. Clarke, O. Grumberg:
“Selective Quantitative Analysis
and Interval Model Checking: Verifying Different Facets of a System“,
Formal Methods in System Design, Volume 17, Number 2, October 2000. Also in CAV’96.
O. Grumberg, R.P. Kurshan:
“Which Branching-Time Properties are Effectively Linear?”,
Logic and Computation, Volume 11, Number 2, April 2001.
D. Bustan, O. Grumberg:
“Simulation Based Minimization “,
ACM Transaction on Computer Logic.
K. Yorav, O. Grumberg:
“Syntax-Directed Model Checking of Sequential Programs “,
Journal of Logic and Algebraic Programming (Special Issue on Model Checking).
T. Heyman, D. Geist, O. Grumberg, A. Schuster:
“Achieving Scalability in Parallel Reachability Analysis of Very Large
Circuits”,
Formal Methods in Systems Design.
S.Livne, O. Grumberg, S. Markovitch:
“Machine Learning for Efficient BDD Variable Ordering in Verification”,
Journal of Artificial Intelligence Research, Volume 18, 2003.
S. Ben-David, T. Heyman, O. Grumberg, A. Schuster,
“Scalable Distributed On-the-fly Symbolic Model Checking”,
International Journal on Software Tools for Technology Transfer (STTT).
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith:
“Counterexample-Guided Abstraction Refinement for Symbolic Model Checking”,
JACM 50(5): 752-794 (2003).
K.Yorav, O.Grumberg:
“Static Analysis for State-Space Reductions Preserving Temporal
Logics“,
Formal Methods in System Design, Volume 25, Issue 1,
July 2004, Pages 67 – 96.
S. Campos, O. Grumberg, K. Yorav and C. Fady:
“Test Sequence Generation and Model Checking Using Dynamic
Transition Relations”,
International Journal on Software Tools for Technology Transfer (STTT), volume 6, number 2, August 2004.
D. Bustan, O. Grumberg:
“Applicability of Fair Simulations”,
Information and Computation, Volume 194, Issue 1, pages 1-18, 2004.
O. Grumberg, T. Heyman, A. Schuster:
“Distributed Model Checking for mu-calculus”,
Formal Methods in System Design, Vol. 26, No. 2, March 2005.
S. Barner, O. Grumberg:
“Combining Symmetry Reduction and Upper-Approximation
for Symbolic Model Checking”,
Formal Methods in System Design, Volume 27, numbers 1/2, September 2005.
O. Grumberg, T. Heyman, A. Schuster:
“A Work-Efficient Distributed Algorithm for Reachability Analysis”,
Formal Methods in System Design, Volume 29,
numbers 2, September 2006, pages 157-176.
L. Fix, O. Grumberg, T. Heyman, A. Schuster:
“Verifying Very Large Industrial Circuits Using 100 Processes and Beyond”,
Special issue of International Journal of Foundations of Computer Science (IJFCS), volume 18, number 1, February 2007.
O. Grumberg, S. Katz:
“VeriTech: a framework for translating among model
description notations “,
International Journal on Software Tools for Technology
Transfer (STTT), Pages 119 – 132, volume 9, number 2, March 2007.
O. Grumberg, M. Lange, M. Leucker, S. Shoham
“When Not Losing Is Better than Winning: Abstraction and Refinement for the Full mu-Calculus”,
Information and Computation, volume 205, issue 8, pages 1130-1148, August 2007.
S. Shoham, O. Grumberg:
“A Game-Based Framework for CTL Counter-Examples and 3-Valued
Abstraction-Refinement”,
ACM Transactions on Computational Logic (TOCL), 9,1, December 2007.
S. Shoham, O. Grumberg:
“Multi-Valued Model Checking Games”,
Special issue JCSS.
S. Shoham, O. Grumberg:
“3-Valued Abstraction: More Precision at Less Cost”,
Information and Computation, Volume 206, number 11, November 2008.
H. Jain, E.M. Clarke, O. Grumberg:
“Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations”,
Formal Method in System Design, volume 35, number 1, August 2009.
S. Shoham, O. Grumberg:
“Compositional Verification and 3-Valued Abstractions Join Forces”,
Information and Computation, volume 208, number 2, February 2010.

Conferences
O.Grumberg, N.Francez, S.Katz:
“Fair Termination of communicating processes”,
proceedings of the 3rd ACM SIGACT-SIGOPS conference on
principle of distributed computing (PODC), Vancouver, Canada, August 1984.
N.Francez, O.Grumberg, S.Katz, A.Pnueli:
“Proving termination of Prolog programs”,
3rd workshop on logics of programs, Brooklyn, New York, June 1985.
E.M.Clarke, S.Bose, M.C.Browne, O.Grumberg:
“The design and verification of finite-state hardware controllers”,
conference on VLSI, Taiwan, 1987.
E.M.Clarke, O.Grumberg:
“Avoiding the state explosion problem in temporal
logic model checking algorithms”,
proceedings of the 6th ACM SIGACT-SIGOPS conference on principle of distributed computing (PODC), Vancouver, Canada, August 1987.
Z.Shtadler, O.Grumberg:
“Network Grammars, Communication Behaviors and Automatic Verification”,
Workshop on Automatic Verification Methods for Finite-State Systems, Grenoble, France, June 1989.
L.Fix, N.Francez, O.Grumberg:
“Semantics-driven decompositions for the
verification of distributed programs”,
IFIP TC2 Working Conference on Programming Concepts and Methods, Sea Gallilee, Israel, April 1990.
G.Shurek, O.Grumberg:
“The Computer-Aided Modular Framework – Motivation, Solutions and Evaluation Criteria”,
Workshop on Computer Aided Verification, Rutgers, NJ, June 1990.
R.Marelly, O.Grumberg:
“GORMEL – Grammar ORiented ModEL checker“,
TR \# 697 Computer Science Dept., Technion, October 1991.
D.Dams, O.Grumberg, R.Gerth:
“Generation of Reduced models for Checking Fragments of CTL”,
CAV, Heraklion, Crete, June 1993.
D.Dams, O.Grumberg, R.Gerth:
“Abstract Interpretation of Reactive Systems: Abstractions Preserving ACTL*, ECTL*, CTL*”,
IFIP working conference on Programming Concepts, Methods
and Calculi (PROCOMET’94), San Miniato, Italy, June 1994.
O. Grumberg, R.P. Kurshan:
“How Linear can branching-time be?”,
the Conference on temporal Logic (ICTL’94), Bonn, Germany, July 1994.
E. Clarke, O. Grumberg, K. McMillan, X. Zhao:
“Efficient generation of counterexamples and witnesses in symbolic model checking”,
the Design Automation Conference 1995 (DAC’95).
G. Bhat, R. Cleaveland, O. Grumberg:
“Efficient On-the-Fly Model Checking for CTL*”, LICS’95.
W. Damm, O. Grumberg, H. Hungar:
“What if Model Checking Must be Truly Symbolic“,
workshop on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS’95), Aarhus, Denmark, May 1995.
E.M. Clarke, O. Grumberg, S. Jha:
“Verifying Parametrized Networks Using Abstraction and Regular Languages“,
6th International Conference on Concurrency Theory (CONCUR’95), Philadelphia, PA, August 1995.
S. Campos, E.M. Clarke, O. Grumberg:
“Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System“,
the Conference on Computer-Aided Verification (CAV’96), Rutgers, NJ, July-August 1996. Also in Formal Methods in System Design.
K. Laster, O. Grumberg:
“Modular Model Checking of Software“,
the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), Lisbon, March-April 1998.
J. Bohn, W. Damm, O. Grumberg, H. Hungar, K. Laster:
“First-Order-CTL Model Checking“,
Foundations of Software Technology and Theoretical Computer Science, Chennai, India (FST & TCS ’98), December 17–19, 1998.
S. Katz, D. Geist, O. Grumberg,
““Have I written enough properties?” –
A method of comparison between specification and implementation“,
CHARME’99, Bad Herrenalb, Germany, September 27-29, 1999.
D. Bustan, O. Grumberg,
“Simulation Based Minimization“,
the 17th International Conference on Automated Deduction (CADE’00), Pittsburgh, June 2000.
E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith,
“Counterexample-guided Abstraction Refinement“,
International Conference on Computer Aided Verification (CAV’00), Chicago, July 2000.
T. Heyman, D. Geist, O. Grumberg, A. Schuster,
“Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits“,
International Conference on Computer Aided Verification (CAV’00), Chicago, July 2000.
D. Dams, R. Gerth, O. Grumberg,
“A heuristic for the automatic generation of ranking functions“,
Workshop on Advances in Verification (WAVE’00),
Chicago, July 2000.
D. Dams, R. Gerth, O. Grumberg,
“Fair Model Checking of Abstractions“,
the workshop on Verification and Computational
Logic (VCL’00), London, July 2000.
S. Ben-David, T. Heyman, O. Grumberg, A. Schuster,
“Scalable Distributed On-the-fly Symbolic Model Checking“,
third International Conference on Formal methods in Computer-Aided Design (FMCAD’00), Austin, Texas, November 2000.
O. Grumberg, T. Heyman, A. Schuster,
“Distributed Symbolic Model checking for Mu-calculus“,
International Conference on Computer Aided Verification (CAV’01), Paris, July 2001.
D. Bustan, O. Grumberg:
“Modular Minimization of Deterministic Finite-State Machines“,
6th International workshop on Formal Methods for Industrial
Critical Systems (FMICS’01), Paris, July 2001.
“Modular Minimization of Finite-State Machines”
is an extended version submitted to a journal.
D. Bustan, O. Grumberg:
“Applicability of Fair Simulations”,
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02) Grenoble, April 2002.
A full version can be found here .
K. Korenblat (Pokozy), O. Grumberg, S. Katz:
“Translations Between Textual Transition Systems and Petri Nets “,
Third International Conference on Integrated Formal Methods (IFM’02), Turku, Finland, May 2002.
S. Barner, O. Grumberg:
“Combining Symmetry Reduction and Upper-Approximation
for Symbolic Model Checking “,
International Conference on Computer Aided Verification (CAV’02), Copenhagen, July, 2002.
S. Shoham, O. Grumberg:
“A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement “,
International Conference on Computer Aided Verification (CAV’03), Bolder, Colorado, July, 2003.
O. Grumberg, T. Heyman, A. Schuster:
“A Work-Efficient Distributed Algorithm for Reachability Analysis “,
International Conference on Computer Aided Verification (CAV’03), Bolder, Colorado, July, 2003.
R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A. Tiemeyer, M. Vardi:
“Enhanced Vacuity Detection in Linear Temporal Logic “,
International Conference on Computer Aided Verification (CAV’03), Bolder, Colorado, July, 2003.
E. Clarke, O. Grumberg, M. Talupur, D. Wang:
“Making Predicate Abstraction Efficient: How to Eliminate Reduntant Predicates “,
International Conference on Computer Aided Verification (CAV’03), Bolder, Colorado, July, 2003.
E. Clarke, O. Grumberg, M. Talupur, D. Wang:
“High Level Verification of Control Intensive Systems Using Predicate Abstraction “,
MEMOCODE’03, June, 2003.
S. Shoham, O. Grumberg:
“Monotonic Abstraction-Refinement for CTL “,
Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’04), Barcelona, April 2004.
O. Grumberg, A. Schuster, A. Yadgar:
“Memory Efficient
All-Solutions SAT solver and its Application to Reachability “,
Fifth International Conference on Formal methods in Computer-Aided Design (FMCAD’04), Austin, Texas, November 2004.
O. Grumberg, F. Lerda, O. Strichman, M. Theobald:
“Underapproximation-Widening for Multi-Process Systems“,
The 32nd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL’05),
Long Beach, California, January 2005.
O. Grumberg, M. Lange, M. Leucker, S. Shoham:
“Don’t Know in Mu-Calculus“,
The 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’05),
Paris, January 2005.
I. Rabinovitz, O. Grumberg:
“Bounded Model Checking of Concurrent Programs“,
International Conference on Computer Aided Verification (CAV’05), Edinburgh, July 2005.
O. Grumberg, T. Heyman, N. Ifergan, A. Schuster:
“Achieving High-Speedups in Distributed Reachability Analysis through Asynchronous Computation “,
Conference on Correct Hardware Design and Verification Methods (CHARME’05),Saarbrucken, Germany, October 2005.
D. Bustan, A. Flaisher, O. Grumberg, O. Kupferman, M. Vardi:
“Regular Vacuity “,
Conference on Correct Hardware Design and Verification Methods (CHARME’05),Saarbrucken, Germany, October 2005.
L. Fix, O. Grumberg, T. Heyman, A. Schuster:
“Verifying Very Large Industrial Circuits Using 100 Processes
and Beyond “,
Third International Symposium on
Automated Technology for Verification and Analysis (ATVA’05),
Taipei, Taiwan, October, 2005.
S. Shoham, O. Grumberg:
“Multi-Valued Model Checking Games “,
Third International Symposium on
Automated Technology for Verification and Analysis (ATVA’05),
Taipei, Taiwan, October, 2005.
S. Shoham, O. Grumberg:
“3-Valued Abstraction: More Precision at Less Cost “,
Twenty-first Annual IEEE Symposium on Logic in Computer Science (LICS’06), Seattle, Washington, August, 2006.
R. Tzoref, O. Grumberg:
“Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation “,
International Conference on Computer Aided Verification (CAV’06), Seattle, Washington, August, 2006.
S. Shoham, O. Grumberg:
“Compositional Verification and 3-Valued Abstractions Join Forces “,
Static Analysis Symposium (SAS’07), Kongens Lyngby, Denmark, August 2007.
O. Grumberg, A. Schuster, A. Yadgar:
“3-Valued Circuit SAT for STE with Automatic Refinement “,
5th International Symposium on Automated Technology for Verification and Analysis (ATVA’07), Tokyo, October 2007.
R. Oshman, O. Grumberg:
“A New Approach to Bounded Model Checking for Branching Time Logics “,
5th International Symposium on Automated Technology for Verification and Analysis (ATVA’07), Tokyo, October 2007.
H. Chockler, O. Grumberg, A. Yadgar:
“Efficient Automatic STE Refinement Using Responsibility “,
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08),
Budapest, March-April 2008.
H. Jain, E.M. Clarke, O. Grumberg:
“Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations “,
Computer-Aided Verification (CAV’08), Princeton, NJ, July 2008.
Y. Meller, O. Grumberg, S. Shoham:
“A Framework for Compositional Verification of Multi-Valued Systems via Abstraction-Refinement “,
7th International Symposium on Automated Technology for Verification and Analysis (ATVA’09), Macao, October 2009.
Y. Vizel, O. Grumberg:
“Interpolation-Sequence Based Model Checking “,
10th International Conference on Formal Methods in Computer-Aided Design (FMCAD’09), Austin, Texas, November 2009.
O. Grumberg, O. Kupferman, S. Sheinvald:
“Variable Automata over Infinite Alphabets “,
4th International Conference on Language and Automata Theory and Applications (LATA’10), Trier, Germany, May 2010.
Y. Meller, O. Grumberg, K. Yorav:
“Applying Software Model Checking Techniques For behavioral UML models “, Formal Methods (FM’12), Paris, France.
S. Sheinvald, O. Grumberg, O. Kupferman:
“Model Checking Systems and Specifications with Parameterized Atomic Propositions”,
10th International Symposium on Automated Technology for Verification and Analysis (ATVA’12), India, October 2012.
Y. Vizel, O. Grumberg, S. Shoham:
“Lazy Abstraction and SAT-Based Reachability for Hardware Model Checking”,
13th International Conference on Formal Methods in Computer-Aided Design (FMCAD’12), Cambridge, England, October 2012.
Y. Vizel, O. Grumberg, S. Shoham:
“Intertwined Forward-Backward Reachability Analysis Using Interpolants”,
Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13), Rome, March-April 2013.
A. Sosnovich, O. Grumberg, G. Nakibly:
“Finding Security Vulnerabilities in a Network Protocol using Parameterized Systems”,
Computer-Aided Verification (CAV’13), Saint Petersburg, Russia, July 2013.
O. Grumberg, O. Kupferman, S. Sheinvald:
“An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications”,
11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13), Vietnam, October 2013.
Y. Meller, O. Grumberg, K. Yorav:
“Verifying Behavioral UML Systems via CEGAR”,
The 11th International Conference on Integrated Formal Methods (iFM 2014), Bertinoro, Italy, September, 2014.
O. Grumberg, O. Kupferman, S. Sheinvald:
“A Game-Theoretic Approach to Simulation of Data-Parameterized Systems”,
12th International Symposium on Automated Technology for Verification and Analysis (ATVA’14), Sidney, Australia, November , 2014.
K. Abd Elkader, O. Grumberg, C.S. Pasareanu, S. Shoham: “Automated Circular Assume-Guarantee Reasoning”,
20th International Symposium on Formal Methods (FM’15), Oslo, June 2015.
Y. Meller, O. Grumberg, K. Yorav:
“Learning-Based Compositional Model Checking of Behavioral UML Systems”,
International Conference on Formal aspects of Component Software (FACS’15), Rio de Janeiro, Brazil, October 2015.
A. Sosnovich, O. Grumberg, G. Nakibly:
“Analyzing Internet Routing Security Using Model Checking”,
International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 20), Fiji Islands, November 2015.
K. Abd Elkader, O. Grumberg, C.S. Pasareanu, S. Shoham:
“Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement”,
Computer-Aided Verification (CAV’16), Toronto, July 2016.
Bat-Chen Rothenberg, Orna Grumberg:
“Sound and Complete Mutation-Based Program Repair”,
21th International Symposium on Formal Methods (FM’16), Limassol, Cyprus, November 2016.
Hadar Frenkel, Orna Grumberg, Sarai Sheinvald:
“An Automata-Theoretic Approach to Modeling Systems and Specifications Over Infinite Data”,
9th NASA Formal Methods Symposium (NFM’17), Moffett Field, CA, USA, May 2017.
Anna Trostanetski, Orna Grumberg, Daniel Kroening:
“Modular Demand-Driven Analysis of Semantic Difference for Program Versions”,
24th Static Analysis Symposium (SAS’17), New York City, NY, USA, 2017.

Book

Publications related to static analysis, abstraction, and modularity in model checking (Not updated and not exhaustive)

Surveys

Journals

Conferences

Publications related to static analysis, abstraction, and modularity in model checking
(Not updated and not exhaustive)