Zhe Dang
Associate Professor
School of Electrical Engineering and Computer Science
Washington State University
Pullman, WA 99164
Email: zdang@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)
Application of thermodynamics in computer science
[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
See your blackboard pages.
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 with AMD.
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 Google.
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)
Cewei Cui
Currently with Amobee
PhD Dissertation: Information-theoretic Metrics, Thermodynamics Metrics, and Applications. July 2016.
Committee: Zhe Dang (co-Advisor), Tom Fischer (co-Advisor), Li Tan (Member)
Eric Wang
PhD Dissertation: Complexity Analysis of Communicating Objects Using
Gurevich Free Energy, May, 2017
Committee: Zhe Dang (co-Advisor), Tom Fischer (co-Advisor), Carl Hauser (Member)
Dmitry Dementyev
(PhD since August 2011). Currently with Google.
William Hutton
Currently with PNNL.
PhD Dissertation: Specificationless intrusion detection
using thermodynamic formalism of free energy. March 2018.
Committee: Zhe Dang (Advisor), Adam Hahn (Member), Carl Hauser (Member)
Publications
**********Papers in Review*********
-
Wang, Xiujun; Mo, Lei; Zheng, Xiao; Dang, Zhe.
[PDF]
Streaming Histogram Publication over Weighted Sliding
Windows Under Differential Privacy
Tsinghua Science and Technology, 2023 (to appear).
-
Liu, Zhi; Wang, Xiujun; Liu, Alex X.; Zheng, Xiao; Zhou, Hao; Hawbani, Ammar; Dang, Zhe.
[PDF]
A Near-optimal Protocol for Continuous Tag Recognition in Mobile RFID Systems.
IEEE/ACM Transactions on Networking, 2023 (to appear).
-
Wang, Xiujun; Liu, Zhi; Gao, Yan; Zheng, Xiao; Dang, Zhe; Shen, Xiaojun.
[PDF]
A Near-Optimal Protocol for the Grouping Problem in RFID systems.
IEEE Transactions on Mobile Computing, 20(4): 1257-1272(2021).
-
Xiujun Wang, Zhi Liu, Susumu Ishihara, Zhe Dang and Jie Li.
[PDF]
A Near-Optimal Protocol for the Subset Selection Problem in RFID Systems.
Proceedings of The 16th International Conference on Mobility, Sensing and
Networking (IEEE MSN 2020). IEEE. (Best Paper Award)
-
Oscar H. Ibarra, Zhe Dang, Qin Li
Accepting runs of two-way finite automata.
Information and Computation, 260: 1--8, 2018.
-
Oscar H. Ibarra, Cewei Cui, Zhe Dang, and Thomas R. Fischer
[PDF]
Lossiness of communication channels modeled by transducers.
International Journal of Computability, 6(2): 165-181, IOS Press, 2017.
-
Cewei Cui, Zhe Dang, Thomas R. Fischer, and Oscar H. Ibarra
[PDF]
Information rate of some classes of nonregular languages:
an automata-theoretic approach.
Information and Computation, 256: 45-61, 2017.
-
William J. Hutton, Zhe Dang and Cewei Cui.
Killing the password, part 1: An exploratory analysis of walking signatures.
IEEE Computing Conference, pp. 808-813, IEEE 2017.
-
Zhe Dang, Thomas R. Fischer, William J. Hutton, Oscar H. Ibarra, Qin Li
Quantifying Communication in Synchronized Languages.
Theoretical Computer Science, 654:33 44(2016).
-
Cewei Cui, Zhe Dang, Thomas R. Fischer, and Oscar H. Ibarra
[PDF]
Execution Information Rate for Some Classes of
Automata.
Information and Computation, 246:20--29, 2016.
-
Cewei Cui and Zhe Dang.
[PDF of longer version]
A Free Energy Foundation of Semantic Similarity in Automata and Languages.
Proc. of SISAP'16, Lecture Notes in Computer Science vol 9939,
pp. 34 47, Springer, 2016.
-
William J. Hutton and Zhe Dang
Specification-based Intrusion Detection
without a Specification.
IEEE HST DHS conference, 2016.
-
Eric Wang and Zhe Dang
A Message-Passing Architecture Without Public Ids using Send-to-Behavior.
IEEE/ACM ASE'15, pp. 902--905, 2015.
-
Zhe Dang, Dmitry Dementyev, Thomas R. Fischer, and William J. Hutton
Security of Numerical Sensors in Automata.
CIAA 2015, Lecture Notes in Computer Science volume 9223, pp. 76--88, Springer, 2015.
-
Zhe Dang, Thomas R. Fischer, William J. Hutton, Oscar H. Ibarra, Qin Li
Quantifying Communication in Synchronized Languages.
COCOON'15, Lecture Notes in Computer Science volume 9198, pp. 635--647, Springer, 2015.
-
Qin Li and Zhe Dang
[PDF]
Sampling Automata and Programs.
Theoretical Computer Science, 577:125--140, 2015.
-
Xiujun Wang, Yusheng Ji, Zhe Dang, Xiao Zheng, and Baohua Zhao
[PDF]
Improved weighted Bloom
filter and space lower bound analysis of algorithms for approximated membership querying
DASFAA'15, Lecture Notes in Computer Science vol 9050, pp. 346--362, Springer, 2015.
-
Xiujun Wang, Xiao Zheng, Zhe Dang, Xuangou Wu, and Baohua Zhao,
[PDF]
Near-optimal approximate duplicate-detection
in data streams over sliding windows for the uniform query frequency or membership likelihood
CBD'14, IEEE, pp. 122-127, 2014.
-
Cewei Cui, Zhe Dang, Thomas R. Fischer, and Oscar H. Ibarra
[PDF]
Information rate of some classes of nonregular languages: an automata-theoretic approach
in MFCS'14, Lecture Notes in Computer Science, volume 8634, pp. 232--243, Springer, 2014.
-
Zhe Dang, Oscar Ibarra and Qin Li.
[PDF]
Sampling a Two-way Finite Automaton,
a book chapter in Automata, Universality, Computation, volume 12 of the
series book: Emergence, Complexity and Computation, pp. 103--115, Springer, 2015
-
Qin Li, Qin-Kai Zeng and Zhe Dang.
[PDF]
A path sensitive type system for information flow,
journal paper, submitted,2014
-
Oscar H. Ibarra, Cewei Cui, Zhe Dang, and Thomas R. Fischer
[PDF]
Lossiness of .communication channels modeled by transducers,
CiE'14 (Computability in Europe), Lecture Notes in Computer Science, vol 8493, pp. 224-233, Springer, 2014.
-
Eric Wang, Cewei Cui, Zhe Dang, Thomas R. Fischer, and Linmin Yang.
[PDF]
Zero-knowledge blackbox testing: where are the faults?
International Journal of Foundations of Computer Science 25(2): 196-218, 2014.
-
Cewei Cui, Zhe Dang, and Thomas R. Fischer
[PDF]
Bit rate of programs.
submitted, 2013.
-
Cewei Cui, Zhe Dang, Thomas R. Fischer, and Oscar H. Ibarra
[PDF]
Similarity in Languages and Programs.
Theoretical Computer Science, 498: 58--75 (2013).
-
Cewei Cui, Zhe Dang, Thomas R. Fischer, and Oscar H. Ibarra
[PDF]
Execution Information Rate for Some Classes of
Automata.
LATA 2013, Lecture Notes in Computer Science vol 7810, pp. 226--237, Springer.
-
Linmin Yang, Cewei Cui, Zhe Dang, and Thomas R. Fischer
[PDF]
An Information-theoretic Complexity Metric
submitted.
**********Edited Book (Proceedings)*********
-
Oscar H. Ibarra and Zhe Dang (Eds.).
Developments in Language Theory
Lecture Notes in Computer Science Vol. 4036, Springer 2006.
-
Oscar H. Ibarra and Zhe Dang (Eds.).
[Springer Link]
Implementation and Application of Automata.
Lecture Notes in Computer Science Vol. 2759, Springer 2003.
**********Journal Papers*********
-
Cewei Cui, Zhe Dang, and Thomas R. Fischer
[PDF]
Typical Paths of a Graph
Fundamenta Informaticae, 110(1-4): 95--109, 2011.
-
Linmin Yang, Zhe Dang, and Thomas R. Fischer
[PDF]
Information Gain of Blackbox Testing
Formal Aspects of Computing, 23(4): 513-539, 2011
-
Linmin Yang, Yong Wang, and Zhe Dang
[PDF]
Automata and Processes on Multisets of Communicating Objects
Natural Computing 9(4):865 - 887 (2010)
-
Linmin Yang, Zhe Dang, and Oscar Ibarra.
[PDF]
Bond computing systems: a biologically inspired and
high-level dynamics model for pervasive computing
Natural Computing, 9(2): 347-364 (2010)
-
Linmin Yang, Zhe Dang, and Oscar Ibarra.
[PDF]
On stateless automata and P systems
International Journal of Foundations of Computer Science,
19(5): 1259-1276 (2008)
-
Oscar Ibarra, Zhe Dang, and Linmin Yang.
[PDF]
On Counter Machines, Reachability Problems, and Diophantine Equations
International Journal of Foundations of Computer Science,
19(4): 919-934 (2008)
-
Zhe Dang, Oscar Ibarra, Cheng Li, Gaoyan Xie
[PDF]
On the Decidability of Model-checking of P Systems
Journal of Automata, Languages, and Combintorics,
11(3): 279 - 298 (2006).
-
Oscar Ibarra, Sara Woodworth, Hsu-Chun Yen and Zhe Dang
[PDF]
On the Computational Power of 1-Deterministic and Sequential P Systems
Fundamenta Informaticae,73(1-2): 133-152 (2006)
-
Oscar Ibarra
and Zhe Dang
[PDF]
On the Solvability of a Class of Diophantine Equations and Applications
Theoretical Computer Science, 352(1-3): 342-346 (2006)
-
Zhe Dang and Oscar Ibarra
[PDF]
On P Systems Operating in Sequential Mode
International Journal of Foundations of Computer Science,
16(5): 867-881 (2005)
-
Oscar Ibarra, Hsu-Chen Yen and Zhe Dang
[PDF]
On various notions of parallelism in P systems
International Journal of Foundations of Computer Science,
16(4): 683-705 (2005).
-
Zhe Dang, Oscar Ibarra and Jianwen Su
[PDF]
On Composition and Lookahead Delegation of
e-Services Modeled by Automata
Theoretical Computer Science, 341(1-3): 344-363 (2005)
-
Zhe Dang, Oscar Ibarra and Zhi-wei Sun
[PDF]
On Two-Way
Nondeterministic Finite Automata with One
Reversal-Bounded Counter
Theoretical Computer Science 330(1): 59-79 (2005).
-
Gaoyan Xie, Cheng Li and Zhe Dang.
[Postscript]
[PDF]
Linear Reachability Problems and
Minimal Solutions to Linear Diophantine Equation Systems.
Theoretical Computer Science 328:203-219 (2004).
-
O. H. Ibarra and Zhe Dang.
[Postscript]
[PDF]
On Two-Way FA with Monotonic Counters and Quadratic
Diophantine Equations.
Theoretical Computer Science
312(2-3): 359-378 (2004).
-
O. H. Ibarra, Zhe Dang, and O. Egecioglu.
[Postscript]
[PDF]
Catalystic systems, semilinear sets, and vector addition systems.
Theoretical Computer Science
312(2-3): 379-399 (2004).
-
Zhe Dang, T. Bultan, O. H. Ibarra, and R. A. Kemmerer.
[Postscript]
[PDF]
Past timed automata and safety verification.
Theoretical Computer Science
313(1): 57-71 (2004).
-
Zhe Dang.
[PDF]
Pushdown time automata: a binary reachability characterization
and safety verification.
Theoretical Computer Science,
Vol 302, Issues 1-3,
pp 93 - 121, 2003.
-
Oscar H. Ibarra and Zhe Dang.
[Postscript]
[PDF]
Eliminating the Storage Tape in Reachability Constructions.
Theoretical Computer Science
299(1-3): 687-706 (2003).
-
Zhe Dang, Pierluigi San Pietro, and Richard
A. Kemmerer.
[Postscript]
[PDF]
Presburger liveness verification for discrete timed automata.
Theoretical Computer Science, vol 299, pp. 413-438, 2003.
-
Zhe Dang, Oscar H. Ibarra, and Richard
A. Kemmerer.
[Postscript]
[PDF]
Generalized discrete timed automata: dcidable
approximations for safety verification.
Theoretical Computer Science, vol 296 (1), February 2003, pp. 59-74.
-
Oscar H. Ibarra, Zhe Dang and Pierluigi San Pietro.
[Postscript]
[PDF]
Verification in loosely synchronous queue-connected discrete timed automata.
Theoretical Computer Science, vol. 290 (3), January 2003,
pp. 1713-1735.
-
Zhe Dang and Oscar H. Ibarra.
[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.
-
Oscar H. Ibarra, Jianwen Su, Zhe Dang,
Tevfik Bultan and Richard A. Kemmerer.
[Postscript]
[PDF]
Counter Machines and Verification Problems.
Theoretical Computer Science, vol. 289 (1), October 2002, pp. 165-189.
-
Paul Z. Kolano, Zhe Dang, and Richard A. Kemmerer.
[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*********
-
Linmin Yang, Zhe Dang,
Thomas R. Fischer, Min Sik Kim, and Li Tan.
[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
-
Linmin Yang, Zhe Dang, and
Thomas R. Fischer.
[PDF]
A syntax-independent complexity metric
TMFCS'10, 127-134, 2010
-
Linmin Yang, Zhe Dang, and
Thomas R. Fischer.
[PDF]
Optimal Software Testing - A Cooling Down Process
FCS'09, 162-168, 2009
-
Linmin Yang, Yong Wang, and
Zhe Dang.
[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.
-
Linmin Yang, Zhe Dang, and Oscar Ibarra.
[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.
-
Linmin Yang, Zhe Dang, and Oscar Ibarra.
[PDF]
On stateless automata and P systems
ACM'07, Budapest, Hungary, August, 2007, pp. 144-157.
-
Cheng Li and Zhe Dang.
[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.
-
Shuohao Zhang, Curtis E. Dyreson and Zhe Dang.
[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.
-
Cheng Li, Zhe Dang, Oscar Ibarra, and Hsu-Chen Yen.
[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.
-
Zhe Dang, O. Ibarra, S. Woodworth and H. Yen.
[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.
-
Zhe Dang, Oscar Ibarra, Cheng Li and Gaoyan Xie.
[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.
-
Gaoyan Xie and Zhe Dang.
[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.
-
Oscar Ibarra, Sara Woodworth, Hsu-Chen Yen, and Zhe Dang.
[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.
-
Gaoyan Xie and
and Zhe Dang.
[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.
-
Oscar Ibarra, Hsu-Chen Yen, and Zhe Dang.
[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.
-
Zhe Dang, Oscar Ibarra, Pierluigi San Pietro and
Gaoyan Xie
[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.
-
Gaoyan Xie and Zhe Dang
[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.
-
Zhe Dang, Oscar H. Ibarra and Jianwen Su
[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.
-
Zhe Dang and Oscar H. Ibarra
[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.
- Gaoyan Xie, Cheng Li,
and Zhe Dang.
[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.
-
Oscar H. Ibarra, Zhe Dang, Omer Egecioglu and Gaurav Saxena.
[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.
-
Gaoyan Xie, Cheng Li,
and Zhe Dang.
[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.
-
Gaoyan Xie, Zhe Dang,
Oscar H. Ibarra and Pierluigi San Pietro.
[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.
-
Gaoyan Xie, Zhe Dang and
Oscar H. Ibarra.
[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.
-
Pierluigi San Pietro and Zhe Dang.
[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.
-
Oscar H. Ibarra, Zhe Dang and Zhi-wei Sun.
[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.
-
Zhe Dang, Oscar H. Ibarra and Zhi-wei Sun.
[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.
-
Zhe Dang, Oscar H. Ibarra and Pierluigi San Pietro.
[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.
-
Oscar H. Ibarra and Zhe Dang.
[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.
-
Zhe Dang, Tevfik Bultan, Oscar H. Ibarra and Richard A. Kemmerer.
[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.
-
Zhe Dang, Oscar H. Ibarra and Richard A. Kemmerer.
[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.
-
Zhe Dang.
[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.
-
Zhe Dang, Pierluigi San Pietro and R. A. Kemmerer.
[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.
-
Oscar H. Ibarra, Jianwen Su,
Zhe Dang, T. Bultan and R. A. Kemmerer.
[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.
-
Zhe Dang and R. A. Kemmerer.
[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.
-
Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, and Jianwen Su.
[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.
-
Zhe Dang and R. A. Kemmerer.
[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.
-
Zhe Dang and R. A. Kemmerer.
[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.
-
Zhe Dang and R. A. Kemmerer.
[Postscript][PDF]
Using the ASTRAL Model Checker
for Cryptographic Protocol Analysis.
DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.