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)
    • [PDF]

    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 516: Algorithmics (Spring 2012)
    Cpt S 260: Introduction to Computer Architecture (Spring 2012)



    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 (MS since 2001, PhD 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 Currently with Amazon.
    PhD Dissertation: Entropy and Software Systems -- towards an Information-theoretic Foundation of Software Testing, April, 2011
    Committee: Zhe Dang (co-Advisor), Tom Fischer (co-Advisor), Min Sik Kim (Member)


  • Eric Wang (since August 2009). Continuing.


  • Cewei Cui (MS since 2010, PhD since August 2011). 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.



    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. Linmin Yang, Zhe Dang, and Thomas R. Fischer
      4. [PDF]
      An Information-theoretic Complexity Metric
      submitted, 2011.


    4. Cewei Cui, Zhe Dang, and Thomas R. Fischer
      5. [PDF]
      Typical Paths of a Graph
      Fundamenta Informaticae (accepted), 2011.


    5. Linmin Yang, Zhe Dang, and Thomas R. Fischer
      6. [PDF]
      Information Gain of Blackbox Testing
      Formal Aspects of Computing (accepted), 2011


    6. Linmin Yang, Yong Wang, and Zhe Dang
      7. [PDF]
      Automata and Processes on Multisets of Communicating Objects
      Natural Computing 9(4):865 - 887 (2010)


    7. Linmin Yang, Zhe Dang, and Oscar Ibarra.
      8. [PDF]
      Bond computing systems: a biologically inspired and high-level dynamics model for pervasive computing
       Natural Computing, 9(2): 347-364 (2010)



    8. Linmin Yang, Zhe Dang, and Oscar Ibarra.
      9. [PDF]
      On stateless automata and P systems
       International Journal of Foundations of Computer Science, 19(5): 1259-1276 (2008)



    9. Oscar Ibarra, Zhe Dang, and Linmin Yang.
      10. [PDF]
      On Counter Machines, Reachability Problems, and Diophantine Equations
       International Journal of Foundations of Computer Science, 19(4): 919-934 (2008)


    10. Zhe Dang, Oscar Ibarra, Cheng Li, Gaoyan Xie
      11. [PDF]
      On the Decidability of Model-checking of P Systems
       Journal of Automata, Languages, and Combintorics, 11(3): 279 - 298 (2006).



    11. Oscar Ibarra, Sara Woodworth, Hsu-Chun Yen and Zhe Dang
      12. [PDF]
      On the Computational Power of 1-Deterministic and Sequential P Systems
       Fundamenta Informaticae,73(1-2): 133-152 (2006)



    12. Oscar Ibarra and Zhe Dang
      13. [PDF]
      On the Solvability of a Class of Diophantine Equations and Applications
      Theoretical Computer Science, 352(1-3): 342-346 (2006)



    13. Zhe Dang and Oscar Ibarra
      14. [PDF]
      On P Systems Operating in Sequential Mode
      International Journal of Foundations of Computer Science, 16(5): 867-881 (2005)



    14. Oscar Ibarra, Hsu-Chen Yen and Zhe Dang
      15. [PDF]
      On various notions of parallelism in P systems
      International Journal of Foundations of Computer Science, 16(4): 683-705 (2005).



    15. Zhe Dang, Oscar Ibarra and Jianwen Su
      16. [PDF]
      On Composition and Lookahead Delegation of e-Services Modeled by Automata
      Theoretical Computer Science, 341(1-3): 344-363 (2005)


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


    17. Gaoyan Xie, Cheng Li and Zhe Dang.
      18. [Postscript] [PDF]
      Linear Reachability Problems and Minimal Solutions to Linear Diophantine Equation Systems.
      Theoretical Computer Science 328:203-219 (2004).


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


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


    20. Zhe Dang, T. Bultan, O. H. Ibarra, and R. A. Kemmerer.
      21. [Postscript] [PDF]
      Past timed automata and safety verification.
      Theoretical Computer Science 313(1): 57-71 (2004).


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


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


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


    24. Zhe Dang, Oscar H. Ibarra, and Richard A. Kemmerer.
      25. [Postscript] [PDF]
      Generalized discrete timed automata: dcidable approximations for safety verification.
      Theoretical Computer Science, vol 296 (1), February 2003, pp. 59-74.



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


    26. Zhe Dang and Oscar H. Ibarra.
      27. [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.


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


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




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


    29. Linmin Yang, Zhe Dang, Thomas R. Fischer, Min Sik Kim, and Li Tan.
      30. [PDF]
      Entropy and Software Systems -- towards an Information-theoretic Foundation of Software Testing
      Proceedings of FSE/SDP workshop on the future of software engineering research, November 2010

    30. Linmin Yang, Zhe Dang, and Thomas R. Fischer.
      31. [PDF]
      A syntax-independent complexity metric
      TMFCS'10, 127-134, 2010

    31. Linmin Yang, Zhe Dang, and Thomas R. Fischer.
      32. [PDF]
      Optimal Software Testing - A Cooling Down Process
      FCS'09, 162-168, 2009

    32. Linmin Yang, Yong Wang, and Zhe Dang.
      33. [PDF]
      Service Automata on Multisets of Communicating Objects
      Proceedings of the 7th International Conference on Unconventional Computation (UC'08),
      Lecture Notes in Computer Science, Vol. 5204, pp. 242-257, Springer, 2008.

    33. Linmin Yang, Zhe Dang, and Oscar Ibarra.
      34. [PDF]
      Bond computing systems: a biologically inspired and high-level dynamics model for pervasive computing
      Proceedings of the 6th International Conference on Unconventional Computation (UC'07)
      Lecture Notes in Computer Science, Vol. 4618, pp. 226-241, Springer, 2007.

    34. Linmin Yang, Zhe Dang, and Oscar Ibarra.
      35. [PDF]
      On stateless automata and P systems
      ACM'07, Budapest, Hungary, August, 2007, pp. 144-157.

    35. Cheng Li and Zhe Dang.
      36. [PDF]
      Decompositional Algorithms for Safety Verification and Testing of Aspect-Oriented Systems
      FATES'06.
      Lecture Notes in Computer Science, Vol. 4262, pp. 100-114, Springer, 2006.

    36. Shuohao Zhang, Curtis E. Dyreson and Zhe Dang.
      37. [PDF]
      Compacting XML Data
      Proceedings of the 11th International Conference on Database Systems for Advanced Applications (DASFAA'06).
      Lecture Notes in Computer Science, Vol. 3882, pp. 767-776, Springer, 2006.

    37. Cheng Li, Zhe Dang, Oscar Ibarra, and Hsu-Chen Yen.
      38. [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.


    38. Zhe Dang, O. Ibarra, S. Woodworth and H. Yen.
      39. [PDF]
      On Symport/Antiport Systems and Semilinear Sets.
      Proceedings of the 6th International Workshop on Membrane Computing (WMC6).
      Lecture Notes in Computer Science, Vol. 3850, pp. 253-271, Springer, 2005.


    39. Zhe Dang, Oscar Ibarra, Cheng Li and Gaoyan Xie.
      40. [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, Vol. 3699, pp. 82-93, Springer, 2005.


    40. Gaoyan Xie and Zhe Dang.
      41. [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, Vol. 3997, pp. 170-186, Springer, 2005.


    41. Oscar Ibarra, Sara Woodworth, Hsu-Chen Yen, and Zhe Dang.
      42. [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, Vol. 3595, pp. 905-914, Springer, 2005.


    42. Gaoyan Xie and and Zhe Dang.
      43. [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.


    43. Oscar Ibarra, Hsu-Chen Yen, and Zhe Dang.
      44. [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.


    44. Zhe Dang, Oscar Ibarra, Pierluigi San Pietro and Gaoyan Xie
      45. [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.


    45. Gaoyan Xie and Zhe Dang
      46. [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.


    46. Zhe Dang, Oscar H. Ibarra and Jianwen Su
      47. [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.


    47. Zhe Dang and Oscar H. Ibarra
      48. [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.


    48. Gaoyan Xie, Cheng Li, and Zhe Dang.
      49. [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.


    49. Oscar H. Ibarra, Zhe Dang, Omer Egecioglu and Gaurav Saxena.
      50. [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.


    50. Gaoyan Xie, Cheng Li, and Zhe Dang.
      51. [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.


    51. Gaoyan Xie, Zhe Dang, Oscar H. Ibarra and Pierluigi San Pietro.
      52. [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.


    52. Gaoyan Xie, Zhe Dang and Oscar H. Ibarra.
      53. [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.


    53. Pierluigi San Pietro and Zhe Dang.
      54. [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.


    54. Oscar H. Ibarra, Zhe Dang and Zhi-wei Sun.
      55. [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.


    55. Zhe Dang, Oscar H. Ibarra and Zhi-wei Sun.
      56. [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.


    56. Zhe Dang, Oscar H. Ibarra and Pierluigi San Pietro.
      57. [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.


    57. Oscar H. Ibarra and Zhe Dang.
      58. [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.


    58. Zhe Dang, Tevfik Bultan, Oscar H. Ibarra and Richard A. Kemmerer.
      59. [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.


    59. Zhe Dang, Oscar H. Ibarra and Richard A. Kemmerer.
      60. [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.


    60. Zhe Dang.
      61. [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.


    61. Zhe Dang, Pierluigi San Pietro and R. A. Kemmerer.
      62. [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.


    62. Oscar H. Ibarra, Jianwen Su, Zhe Dang, T. Bultan and R. A. Kemmerer.
      63. [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.


    63. Zhe Dang and R. A. Kemmerer.
      64. [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.


    64. Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, and Jianwen Su.
      65. [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.


    65. Zhe Dang and R. A. Kemmerer.
      66. [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.


    66. Zhe Dang and R. A. Kemmerer.
      67. [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.


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