Publications

Book

• 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, 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. To appear in 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.

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, 2009. To Appear.

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'',
  accepted to 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.

  ---