Zhe Dang


Associate Professor
School of Electrical Engineering and Computer Science
Washington State University
Pullman, WA 99164
Email: zdang@eecs.wsu.edu
Phone: 509-335-7238

Research Interests

  • Model-checking and testing for infinite-state and/or real-time systems
  • Automata theory and Membrane computing systems (P systems)

    • Education

    PhD Dissertation: Debugging and Verification of Infinite State Real-time Systems
    Department of Computer Science
    University of California at Santa Barbara
    June, 2000
    Committee: Richard A. Kemmerer (Advisor), Tevfik Bultan (Co-advisor), Oscar H. Ibarra (Member)


    MS Thesis: Using the ASTRAL Model Checker for Cryptographic Protocol Analysis
    Department of Computer Science
    University of California at Santa Barbara
    January, 1998
    Committee: Richard A. Kemmerer (Advisor), Divyakant Agrawal (Member), Alan G. Konheim (Member)

    Teaching


    Cpt S 317: Automata Theory and Formal Languages (Spring 2008)
    HW#9 solutions online. HW#10 online.

    Cpt S 516: Algorithmics (Spring 2008)
    HW#4 solutions online. HW#5 solutions online.

    Grant

    NSF grant, Oscar Ibarra (CCF-0430945) and Zhe Dang (CCF-0430531), Collaborative Research: New automata theories for analyzing infinite state and membrane computing systems ($250K, Aug. 1, 2004 -- July 31, 2007)

    Award

    ``CEA Young Faculty Recognition", College of Engineering and Architecture (CEA), Washington State University, 2005.

    Program Committee

    Eighth International Conference on Implementation and Application of Automata (CIAA 2003)

    Tenth International Conference on Development in Language Theory (DLT 2006)

    PhD Students

  • Gaoyan Xie (January 2002 to July 2005). Current position: Tenure-track Assistant Professor of Computer Science, University of Massachusetts at Dartmouth.

    PhD Dissertation: Fundamental Studies on Automatic Verification of Component-based Systems -- A Decompositional and Hybrid Approach, July, 2005
    Committee: Zhe Dang (Advisor), Anneliese Andrews (Member), Curtis Dyreson (Member)

  • Cheng Li (since January 2003). Currently with Motorola.


  • Yong Wang Currently with Google.
    PhD Dissertation: Clustering, Grouping and Processes over Networks, December, 2007
    Committee: Zhe Dang (co-Advisor), Min Sik Kim (co-Advisor), K C Wang (Member)


  • Linmin Yang (since January 2007). Continuing.



    • Publications


      **********Edited Book (Proceedings)*********


    1. Oscar H. Ibarra and Zhe Dang (Eds.).
      2. Developments in Language Theory
      Lecture Notes in Computer Science Vol. 4036, Springer 2006 (to appear).



    2. Oscar H. Ibarra and Zhe Dang (Eds.).
      3. [Springer Link]
      Implementation and Application of Automata.
      Lecture Notes in Computer Science Vol. 2759, Springer 2003.


      **********Journal Papers*********


    3. Zhe Dang, Oscar Ibarra, Cheng Li, Gaoyan Xie
      4. [PDF]
      On Model-checking of P Systems
       Journal of Automata, Languages, and Combintorics (minor revision sent).



    4. Oscar Ibarra, Sara Woodworth, Hsu-Chun Yen and Zhe Dang
      5. [PDF]
      On the Computational Power of 1-Deterministic and Sequential P Systems
       Fundamenta Informaticae (to appear).



    5. Oscar Ibarra and Zhe Dang
      6. [PDF]
      On the Solvability of a Class of Diophantine Equations and Applications
      Theoretical Computer Science (to appear).



    6. Zhe Dang and Oscar Ibarra
      7. [PDF]
      On P Systems Operating in Sequential Mode
      Invited submission to the special issue of papers selected from DCFS'04.
      Accepted by International Journal of Foundations of Computer Science, 2005.



    7. Oscar Ibarra, Hsu-Chen Yen and Zhe Dang
      8. [PDF]
      On various notions of parallelism in P systems
      Invited submission to the special issue of papers selected from DLT'04.
      International Journal of Foundations of Computer Science, 16(4): 683-705 (2005).



    8. Zhe Dang, Oscar Ibarra and Jianwen Su
      9. [PDF]
      On Composition and Lookahead Delegation of e-Services Modeled by Automata
      Accepted by Theoretical Computer Science. 2005.


    9. Zhe Dang, Oscar Ibarra and Zhi-wei Sun
      10. [PDF]
      On Two-Way Nondeterministic Finite Automata with One Reversal-Bounded Counter
      Theoretical Computer Science 330(1): 59-79 (2005).


    10. Gaoyan Xie, Cheng Li and Zhe Dang.
      11. [Postscript] [PDF]
      Linear Reachability Problems and Minimal Solutions to Linear Diophantine Equation Systems.
      Invited submission to the special issue of papers selected from CIAA'03.
      Accepted by Theoretical Computer Science. 2004.


    11. O. H. Ibarra and Zhe Dang.
      12. [Postscript] [PDF]
      On Two-Way FA with Monotonic Counters and Quadratic Diophantine Equations.
      Theoretical Computer Science 312(2-3): 359-378 (2004).


    12. O. H. Ibarra, Zhe Dang, and O. Egecioglu.
      13. [Postscript] [PDF]
      Catalystic systems, semilinear sets, and vector addition systems.
      Theoretical Computer Science 312(2-3): 379-399 (2004).


    13. Zhe Dang, T. Bultan, O. H. Ibarra, and R. A. Kemmerer.
      14. [Postscript] [PDF]
      Past timed automata and safety verification.
      Theoretical Computer Science 313(1): 57-71 (2004).
      (Special issue of papers selected from CIAA'01)



    14. Zhe Dang.
      15. [PDF]
      Pushdown time automata: a binary reachability characterization and safety verification.
      Theoretical Computer Science, Vol 302, Issues 1-3, pp 93 - 121, 2003.


    15. Oscar H. Ibarra and Zhe Dang.
      16. [Postscript] [PDF]
      Eliminating the Storage Tape in Reachability Constructions.
      Theoretical Computer Science 299(1-3): 687-706 (2003).


    16. Zhe Dang, Pierluigi San Pietro, and Richard A. Kemmerer.
      17. [Postscript] [PDF]
      Presburger liveness verification for discrete timed automata.
      Theoretical Computer Science, vol 299, pp. 413-438, 2003.


    17. Zhe Dang, Oscar H. Ibarra, and Richard A. Kemmerer.
      18. [Postscript] [PDF]
      Generalized discrete timed automata: dcidable approximations for safety verification.
      Invited submission to the special issue of papers selected from COCOON'01
      Theoretical Computer Science, vol 296 (1), February 2003, pp. 59-74.



    18. Oscar H. Ibarra, Zhe Dang and Pierluigi San Pietro.
      19. [Postscript] [PDF]
      Verification in loosely synchronous queue-connected discrete timed automata.
      Theoretical Computer Science, vol. 290 (3), January 2003, pp. 1713-1735.


    19. Zhe Dang and Oscar H. Ibarra.
      20. [Postscript] [PDF]
      The Existence of Omega-Chains for Transitive Mixed Linear Relations and Its Applications.
      International Journal of Foundations of Computer Science, Vol. 13, No. 6 (2002) 911-936.


    20. Oscar H. Ibarra, Jianwen Su, Zhe Dang, Tevfik Bultan and Richard A. Kemmerer.
      21. [Postscript] [PDF]
      Counter Machines and Verification Problems.
      Theoretical Computer Science, vol. 289 (1), October 2002, pp. 165-189.


    21. Paul Z. Kolano, Zhe Dang, and Richard A. Kemmerer.
      22. [Postscript] [PDF]
      The Design and Analysis of Real-Time Systems Using the ASTRAL
      Software Development Environment.
      Annals of Software Engineering 7: 177-210 (1999)


      **********Incomplete list of Journal Papers under Review*********


    22. Gaoyan Xie, Zhe Dang, Oscar Ibarra, and Pierluigi San Pietro
      23. [PDF]
      Reachability problems for dense counter machines
      Information and Computation
      Submitted: Dec 2003. Two positive reviews received in 2005. Under revision.


    23. Gaoyan Xie, Zhe Dang and Oscar Ibarra
      24. [PDF]
      Quadratic Diophantine Equations and Verification of Infinite-state Systems with Parameterized Constants
      Information and Computation
      Submitted: Dec 2003.


      **********Conference and Workshop Papers*********


    24. Cheng Li and Zhe Dang.
      25. [PDF]
      Decompositional Algorithms for Safety Verification and Testing of Aspect-Oriented Systems
      FATES'06.
      Lecture Notes in Computer Science, Springer. 2006 (to appear).

    25. Shuohao Zhang, Curtis E. Dyreson and Zhe Dang.
      26. [PDF]
      Compacting XML Data
      Proceedings of the 11th International Conference on Database Systems for Advanced Applications (DASFAA'06).
      Lecture Notes in Computer Science, Springer. 2006 (to appear).

    26. Cheng Li, Zhe Dang, Oscar Ibarra, and Hsu-Chen Yen.
      27. [PDF] (final version)
      [PDF] (long version)
      Signaling P Systems and Verification Problems
      Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05),
      Lecture Notes in Computer Science, Vol. 3580, pp. 1462--1473, Springer. 2005.


    27. Zhe Dang, O. Ibarra, S. Woodworth and H. Yen.
      28. [PDF]
      On Symport/Antiport Systems and Semilinear Sets.
      Proceedings of the 6th International Workshop on Membrane Computing (WMC6).
      Lecture Notes in Computer Science, Springer. 2005 (to appear).


    28. Zhe Dang, Oscar Ibarra, Cheng Li and Gaoyan Xie.
      29. [PDF] (final version)
      [PDF] (originally submitted long version, with SPIN and Omega code)
      Model-checking of P systems
      Proceedings of the 4th International Conference on Unconventional Computation (UC'05),
      Lecture Notes in Computer Science, Springer. 2005 (to appear).


    29. Gaoyan Xie and Zhe Dang.
      30. [PDF]
      Testing Systems of Concurrent Black-boxes---an Automata-Theoretic Approach
      Proceedings of the 5th Workshop on Formal Approaches to Testing Software (FATES'05),
      Lecture Notes in Computer Science, Springer. 2005 (to appear).


    30. Oscar Ibarra, Sara Woodworth, Hsu-Chen Yen, and Zhe Dang.
      31. [PDF] (originally submitted version)
      On Sequential and 1-Deterministic P Systems
      Proceedings of the 11th International Computing and Combinatorics Conference (COCOON'05),
      Lecture Notes in Computer Science, Springer. 2005 (to appear).


    31. Gaoyan Xie and and Zhe Dang.
      32. [PDF]
      CTL model-checking for systems with unspecified finite state components
      Proceedings of the 3rd workshop on specification and verification of component-based systems (SAVCBS'04), affiliated with ACM SIGSOFT 2004/FSE-12, ISU TR \#04-09, pp. 32-38, 2004.


    32. Oscar Ibarra, Hsu-Chen Yen, and Zhe Dang.
      33. [PDF]
      The Power of Maximal Parallelism in P Systems
      Proceedings of the 8th International Conference on Developments in Language Theory (DLT'04),
      Lecture Notes in Computer Science, Vol. 3340, pp. 212-224, Springer, 2004.


    33. Zhe Dang, Oscar Ibarra, Pierluigi San Pietro and Gaoyan Xie
      34. [PDF]
      Real-Counter Automata And Their Decision Problems
      Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04),
      Lecture Notes in Computer Science, Vol. 3328, pp. 198-210, Springer, 2004.


    34. Gaoyan Xie and Zhe Dang
      35. [PDF]
      An Automata-theoretic Approach for Model-checking Systems with Unspecified Components
      Proceedings of the 4th International Workshop on Formal Approaches to Software Testing (FATES'04),
      Lecture Notes in Computer Science, Vol. 3395, pp. 155-169, Springer, 2004.


    35. Zhe Dang, Oscar H. Ibarra and Jianwen Su
      36. [PDF]
      Composability of Infinite-State Activity Automata
      Proceedings of the 15th International Symposium on Algorithms and Computation (ISAAC'04),
      Lecture Notes in Computer Science, Vol. 3341, pp. 377-388, Springer, 2004.


    36. Zhe Dang and Oscar H. Ibarra
      37. [Postscript] [PDF]
      On P Systems Operating in Sequential Mode
      Preproceedings of the 6th Workshop on Descriptional Complexity of Formal Systems (DCFS'04), (L. Ilie, D. Wotschke, eds.), Report No. 619, Univ. of Western Ontario, London, Canada (2004), 164-177.


    37. Gaoyan Xie, Cheng Li, and Zhe Dang.
      38. [Postscript] [PDF] (long version)
      Testability of Oracle Automata
      Proceedings of the 9th International Conference on Implementation and Application of Automata (CIAA'04),
      Lecture Notes in Computer Science, Vol. 3317, pp. 331-332, Springer, 2004.


    38. Oscar H. Ibarra, Zhe Dang, Omer Egecioglu and Gaurav Saxena.
      39. [Postscript] [PDF]
      Characterizations of Catalytic Membrane Computing Systems.
      Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS'03),
      Lecture Notes in Computer Science Vol. 2747, pp. 480--489, Springer. 2003.


    39. Gaoyan Xie, Cheng Li, and Zhe Dang.
      40. [Postscript] [PDF]
      New Complexity Results for Some Linear Counting Problems Using Minimal Solutions to Linear Diophantine Equations.
      Proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA'03),
      Lecture Notes in Computer Science Vol. 2759, pp. 163--175, Springer. 2003.


    40. Gaoyan Xie, Zhe Dang, Oscar H. Ibarra and Pierluigi San Pietro.
      41. [PDF]
      Dense counter machines and verification problems.
      Proceedings of the 15th International Conference on Computer Aided Verification (CAV'03),
      Lecture Notes in Computer Science Vol. 2725, pp. 93--105, Springer. 2003.


    41. Gaoyan Xie, Zhe Dang and Oscar H. Ibarra.
      42. [PDF]
      A solvable class of quadratic Diophantine equations with applications to verification of infinite state systems.
      Proceedings of the 30th International Colloquium on Automata, Languages and Programming (ICALP'03),
      Lecture Notes in Computer Science Vol. 2719, pp. 668--680, Springer. 2003.


    42. Pierluigi San Pietro and Zhe Dang.
      43. [Postscript] [PDF]
      Automatic verification of multi-queue discrete timed automata
      Proceedings of the 9th Annual International Conference on Computing and Combinatorics (COCOON'03),
      Lecture Notes in Computer Science Vol. 2697, pp. 159--171, Springer. 2003.


    43. Oscar H. Ibarra, Zhe Dang and Zhi-wei Sun.
      44. [Postscript] [PDF]
      Safety Verification for Two-Way Finite Automata with Monotonic Counters
      Proceedings of the 6th International Conference on Developments in Language Theory (DLT'02),
      Lecture Notes in Computer Science Vol. 2450, pp. 326--338, Springer. 2002.


    44. Zhe Dang, Oscar H. Ibarra and Zhi-wei Sun.
      45. [Postscript] [PDF]
      On the Emptiness Problem for Two-way NFA with One Reversal-Bounded Counter
      Proceedings of the 13th International Symposium on Algorithms and Computation (ISAAC'02),
      Lecture Notes in Computer Science vol 2518, pp. 103--114, Springer. 2002.


    45. Zhe Dang, Oscar H. Ibarra and Pierluigi San Pietro.
      46. [Postscript] [PDF]
      Liveness Verification of Reversal-bounded Multicounter Machines
      with a Free Counter.
      Proceedings of the 20th International Conference on Foundations of
      Software Technology and Theoretical Computer Science (FSTTCS 2001)
      Lecture Notes in Computer Science vol 2245, pp. 132-143, Springer. 2001.


    46. Oscar H. Ibarra and Zhe Dang.
      47. [Postscript] [PDF]
      On removing the stack from reachability constructions
      with applications to Presburger LTL satisfiability-checking.
      Proceedings of the International Symposium on
      Algorithms and Computation (ISAAC 2001),
      Lecture Notes in Computer Science vol 2223, pp. 244-256, Springer. 2001.


    47. Zhe Dang, Tevfik Bultan, Oscar H. Ibarra and Richard A. Kemmerer.
      48. [Postscript] [PDF]
      Past Pushdown Timed Automata.
      Proceedings of the 6th International Conference on Implementation and
      Application of Automata (CIAA 2001)
      Lecture Notes in Computer Science 2494, pp. 74--86, Springer. 2002.


    48. Zhe Dang, Oscar H. Ibarra and Richard A. Kemmerer.
      49. [Postscript] [PDF]
      Decidable Approximations on Generalized and Parameterized Discrete Timed Automata.
      Proceedings of the 7th Annual International Computing and
      Combinatorics Conference (COCOON 2001),
      Lecture Notes in Computer Science 2108, pp. 529-539, Springer.


    49. Zhe Dang.
      50. [Postscript] [PDF]
      Binary reachability analysis of pushdown timed automata with dense clocks.
      Proceedings of the 13th International Conference on
      Computer Aided Verification (CAV 2001),
      Lecture Notes in Computer Science 2102, pp. 506 - 517, Springer.


    50. Zhe Dang, Pierluigi San Pietro and R. A. Kemmerer.
      51. [Postscript] [PDF]
      On Presburger Liveness of Discrete Timed Automata.
      Proceedings of the 18th International Symposium on
      Theoretical Aspects of Computer Science (STACS 2001)
      Lecture Notes in Computer Science 2010, pp. 132-143, Springer.


    51. Oscar H. Ibarra, Jianwen Su, Zhe Dang, T. Bultan and R. A. Kemmerer.
      52. [Postscript] [PDF]
      Counter Machines: Decidable Properties and Applications to Verification Problems.
      Proceedings of the 25th International Symposium on
      Mathematical Foundations of Computer Science (MFCS 2000),
      Lecture Notes in Computer Science 1893, pp. 426-435, Springer.


    52. Zhe Dang and R. A. Kemmerer.
      53. [Postscript] [PDF]
      Using the ASTRAL Symbolic Model Checker as a Specification Debugger:
      Three Approximation Techniques.
      Proceedings of the 22nd International Conference on
      Software Engineering (ICSE 2000),
      pp. 345-354, IEEE Press.


    53. Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, and Jianwen Su.
      54. [Postscript] [PDF]
      Binary Reachability Analysis of Discrete Pushdown Timed Automata.
      Proceedings of the 12th International Conference on
      Computer Aided Verification (CAV 2000),
      Lecture Notes in Computer Science 1855, pp. 69-84, Springer.


    54. Zhe Dang and R. A. Kemmerer.
      55. [Postscript] [PDF]
      Using the ASTRAL Model Checker to Analyze Mobile IP.
      Proceedings of the 21st International Conference on
      Software Engineering (ICSE 99),
      pp. 132-141, IEEE Press.


    55. Zhe Dang and R. A. Kemmerer.
      56. [Postscript] [PDF]
      A symbolic model checker for testing ASTRAL real-time specifications.
      Proceedings of the 6th International Conference on
      Real-Time Computing Systems and Applications (RTCSA'99),
      pp. 174-181, IEEE Press.


    56. Zhe Dang and R. A. Kemmerer.
      57. [Postscript][PDF]
      Using the ASTRAL Model Checker for Cryptographic Protocol Analysis.
      DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.