Publications

2009

Yang Cai, Ting Zhang, Haifeng Luo. An Improved Lower Bound for the Complementation of Rabin Automata. In the Proceedings of the Symposium on Logic in Computer Science (LICS 2009), pp. 167-176, IEEE Press, August, 2009.

2008

Jiamou Liu, Ting Zhang. Towards Combining Dense Linear Orders with Random Graphs. In Proc. Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08).

2007

Ting Zhang, Henny B. Sipma, Zohar Manna, The Decidability of the First-order Theory of Knuth-Bendix Order. Submitted.
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.

2006

Ting Zhang, Arithmetic Integration of Decision Procedures. Ph.D. Thesis, 06.06.06.

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.

2005

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 Science (FSTTCS 2005), Lecture Notes in Computer Science, vol. 3821, pp. 225-237, Springer-Verlag, 2005.

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.

2004

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.

Grigori Mints, Ting Zhang, Dynamical topological logic of Cantor space (Abstract), Bulletin of the ASL, vol. 10, no. 2, pp. 288-289, 2004.

2003

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.

Grigori Mints, Ting Zhang, A proof of topological completeness of S4 in (0,1) (Abstract). Bulletin of the ASL, vol. 9, no. 2, pp. 248-249, 2003.

2001

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

2000

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.

Home Talks