Benny Godlin

Contact Details:

Phone: +972-4-836-6088
Fax: +972-4-911-8046
Email: bgodlin <AT>

Currently, I am an independent researcher in the area of hierarchical graphs, i.e. graphs which can be decomposed into or are created from modules which are reused several times in the hierarchy. I am interested in their representation, mathematical properties, their recognition and decomposition, and efficient algorithms for solving logical and quantitative problems on them.

The first step in the hierarchical graphs research is the open source HRDAG project used to decompose hierarchical graphs. This may be useful to reverse-engineer human constructs like electronic equipment, manufactured machines, or bureaucratic hierarchies; but also to decompose natural constructs like gene-relation or protein-relation nets.

I am also interested in Software/Hardware Formal Verification, Logic and Graph Theory, Finite Model Theory, and Graph Polynomials.


I hold M.Sc. (2008, Cum Laude) and B.Sc. (1996, Summa Cum Laude) from the Computer Science Department at the Technion - Israel Institute of Technology.

My M.Sc. thesis title: Regression Verification: Theoretical and Implementation Aspects , under the supervision of Prof. Ofer Strichman.


  1. Benny Godlin, Ofer Strichman:
    Regression verification: Proving the equivalence of similar programs.
    (to be published in) Software Testing, Verification and Reliability, 2012.

  2. Benny Godlin, Emilia Katz, Johann A. Makowsky:
    Graph Polynomials: From Recursive Definitions to Subset Expansion Formulas.
    in J. Log. Comput. 22(2): 237-265 (2012)

  3. Benny Godlin, Ofer Strichman:
    Inference Rules for Proving the Equivalence of Recursive Procedures.
    in Essays in Memory of Amir Pnueli 2010: 167-184
    (not peer-reviewed, an extended extract from our ACTA paper below).

  4. Ilya Averbouch, Benny Godlin, Johann A. Makowsky:
    An extension of the bivariate chromatic polynomial.
    in Eur. J. Comb. 31(1): 1-17 (2010)

  5. Benny Godlin, Ofer Strichman: Regression verification.
    in Proc. of DAC 2009: 466-471 and presentation

  6. Hana Chockler, Eitan Farchi, Benny Godlin, Sergey Novikov:
    Cross-Entropy-Based Replay of Concurrent Programs.
    in Proc. of FASE 2009: 201-215

  7. Benny Godlin, Tomer Kotek, Johann A. Makowsky:
    Evaluations of Graph Polynomials.
    in Proc. of WG 2008: 183-194

  8. Ilya Averbouch, Benny Godlin, Johann A. Makowsky:
    A Most General Edge Elimination Polynomial.
    in Proc. of WG 2008: 31-42

  9. Benny Godlin, Ofer Strichman:
    Inference rules for proving the equivalence of recursive procedures.
    in Acta Inf. 45(6): 403-439 (2008) and presentation

  10. Hana Chockler, Eitan Farchi, Benny Godlin, Sergey Novikov:
    Cross-Entropy Based Testing.
    in Proc. of FMCAD 2007: 101-108 and presentation

  11. Hana Chockler, Eitan Farchi, Ziv Glazberg, Benny Godlin, Yarden Nir-Buchbinder, Ishai Rabinovitz:
    Formal verification of concurrent software: two case studies.
    in Proc. of PADTAD 2006: 11-22

  12. Johann A. Makowsky, Udi Rotics, Ilya Averbouch, Benny Godlin:
    Computing Graph Polynomials on Graphs of Bounded Clique-Width.
    in Proc. of WG 2006: 191-204

  13. Ofer Strichman, Benny Godlin:
    Regression Verification - A Practical Way to Verify Programs.
    in Proc. of VSTTE 2005: 496-501 (a position paper).

Work Experience:

See my CV.