Journal Publications
- Ting Zhang, Henny B. Sipma, Zohar Manna,
The Decidability of the First-order Theory of Knuth-Bendix Order.
Submitted.
- Ting Zhang, Henny B. Sipma, Zohar Manna,
Decision Procedures for Term Algebras with Integer Constraints.
Information and Computation, vol. 204, no. 10, pp. 1526-1574, 2006.
- Grigori Mints, Ting Zhang,
A proof of topological completeness of S4 in (0,1).
Annals of Pure and Applied Logic, vol. 133, no. 1-3, pp. 231-245, 2005.
- Grigori Mints, Ting Zhang,
Propositional logic of continuous transformation in Cantor space.
Archive for Mathematical Logic, vol. 44, no. 6, pp. 783-799, 2005.
- Yang Cai, Ting Zhang, Haifeng Luo.
An Improved Lower Bound for the Complementation of Rabin Automata.
To appear in LICS'09.
- Jiamou Liu, Ting Zhang.
Towards Combining Dense Linear Orders with Random Graphs.
In Proc. Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR 2008).
- Zohar Manna, Henny B. Sipma, Ting Zhang.
A Decidable Logic for Trees with Updates.
In preparation.
- Zohar Manna, Henny B. Sipma, Ting Zhang.
Verifying Balanced Trees.
In the Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2007),
Lecture Notes in Computer Science, vol. 4514, pp. 363-378, Springer-Verlag, 2007.
- Ting Zhang, Henny B. Sipma, Zohar Manna,
The Decidability of the First-order Theory of Knuth-Bendix Order.
In the Proceedings of the 20th International Conference on Automated Deduction (CADE 2005), Lecture Notes in Computer Science, vol. 3632, pp. 131-148, Springer-Verlag, 2005.
(Solution to RTA Problem 99)
- Ting Zhang, Henny B. Sipma, Zohar Manna,
Decision Procedures for Queues with Integer Constraints.
In the Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Sciencei (FSTTCS 2005), Lecture Notes in Computer Science, vol. 3821, pp. 225-237, Springer-Verlag, 2005.
- Ting Zhang, Henny B. Sipma, Zohar Manna,
Decision Procedures for Recursive Data Structures with Integer Constraints.
In the Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR 2004), Lecture Notes in Computer Science, vol. 3097, pp. 152-167, Springer-Verlag, 2004.
(Best Paper Award)
- Ting Zhang, Henny B. Sipma, Zohar Manna,
Term Algebras with Length Function and Bounded Quantifier Alternation.
In the Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), Lecture Notes in Computer Science, vol. 3223, pp. 321-336, Springer-Verlag, 2004.
- Cesar Sanchez, Sriram Sankaranarayanan, Henny B. Sipma, Ting Zhang, David Dill, and Zohar Manna.
Event Correlation: Language and Semantics.
In the proceedings of the 3rd International Conference on Embedded Software (EMSOFT 2003), Lecture Notes in Computer Science, vol. 2855, pp. 323-339, Springer-Verlag, 2003.
- Ting Zhang, Luca Benini, Giovanni De Micheli.
Component selection and matching for IP-based design.
In the proceedings of the 4th Conference on Design, Automation and Test in Europe (DATE 2001), pp 40-46, ACM press , 2001
- Anca Browne, Henny B. Sipma, Ting Zhang.
Linking STeP with SPIN.
In the proceedings of the 7th International SPIN Workshop on Model Checking of Software (SPIN 2000), Lecture Notes in Computer Science, vol. 1885, pp. 181-186, Springer-Verlag, 2000.
- Grigori Mints, Ting Zhang,
A proof of topological completeness of S4 in (0,1).
Bulletin of the ASL, vol. 9, no. 2, pp. 248-249, 2003.
- Grigori Mints, Ting Zhang,
Dynamical topological logic of Cantor space.
Bulletin of the ASL, vol. 10, no. 2, pp. 288-289, 2004.