Zhang, Zhihai; Kapur, Deepak On invariant checking. (English) Zbl 1310.68147 J. Syst. Sci. Complex. 26, No. 3, 470-482 (2013). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{Z. Zhang} and \textit{D. Kapur}, J. Syst. Sci. Complex. 26, No. 3, 470--482 (2013; Zbl 1310.68147) Full Text: DOI
Kapur, Deepak; Zhang, Zhihai; Horbach, Matthias; Zhao, Hengjun; Lu, Qi; Nguyen, ThanhVu Geometric quantifier elimination heuristics for automatically generating octagonal and max-plus invariants. (English) Zbl 1385.68013 Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 189-228 (2013). MSC: 68N30 03C10 68T15 PDFBibTeX XMLCite \textit{D. Kapur} et al., Lect. Notes Comput. Sci. 7788, 189--228 (2013; Zbl 1385.68013) Full Text: DOI
Zhang, ZhiHai; Fang, Tian; Xia, BiCan Real solution isolation with multiplicity of zero-dimensional triangular systems. (English) Zbl 1218.65046 Sci. China, Inf. Sci. 54, No. 1, 60-69 (2011). MSC: 65H10 65H04 12D05 12D10 12Y05 65G30 PDFBibTeX XMLCite \textit{Z. Zhang} et al., Sci. China, Inf. Sci. 54, No. 1, 60--69 (2011; Zbl 1218.65046) Full Text: DOI Link
Xia, Bican; Yang, Lu; Zhan, Naijun; Zhang, Zhihai Symbolic decision procedure for termination of linear programs. (English) Zbl 1216.68077 Formal Asp. Comput. 23, No. 2, 171-190 (2011). MSC: 68N30 68W30 PDFBibTeX XMLCite \textit{B. Xia} et al., Formal Asp. Comput. 23, No. 2, 171--190 (2011; Zbl 1216.68077) Full Text: DOI
Xia, Bican; Zhang, Zhihai Termination of linear programs with nonlinear constraints. (English) Zbl 1208.68151 J. Symb. Comput. 45, No. 11, 1234-1249 (2010). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{B. Xia} and \textit{Z. Zhang}, J. Symb. Comput. 45, No. 11, 1234--1249 (2010; Zbl 1208.68151) Full Text: DOI