• E.M.Clarke, O. Grumberg, D. Peled:
    “Model Checking”, MIT Press, December 1999.
    ISBN 0-262-03270-8

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



  • 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,
    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
    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
    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
    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.