People
Education
Ph.D., Sichuan University, 1998.
M.S., Sichuan University, 1993.
B.S., Sichuan University, 1990.
M.S., Sichuan University, 1993.
B.S., Sichuan University, 1990.
Research Interests
Computer algebra, automated reasoning, program verification
1. Algorithms in real algebra and real algebraic geometry
2. Automated proving and discovering of inequalities
3. Program and hybrid system verification
1. Algorithms in real algebra and real algebraic geometry
2. Automated proving and discovering of inequalities
3. Program and hybrid system verification
Selected Publication
B. Xia and L. Yang: Automated Inequality Proving and Discovering. World Scientific, 344 pages, Aug. 2016.
T. Gan, L. Dai, B. Xia, N. Zhan, D. Kapur and M. Chen: Interpolation synthesis for quadratic polynomial inequalities and combination with EUF. N. Olivetti and A. Tiwari (Eds.): IJCAR 2016, LNAI 9706, pp. 195–212, 2016.
J. Han, Z. Jin and B. Xia: Proving Inequalities and Solving Global Optimization Problems via Simplified CAD Projection. Journal of Symbolic Computation, vol. 72, pp. 206--230, 2016.
J. Han, L. Dai and B. Xia: Constructing Fewer Open Cells by GCD Computation in CAD Projection. In: Proc. ISSAC 2014, 240--247, ACM Press, 2014.
L. Dai, B. Xia and N. Zhan: Generating non-linear interpolants by semi-definite programming. In: N. Sharygina and H. Veith (Eds.): CAV 2013, LNCS 8044, pp. 364--380, Springer, Heidelberg (2013).
T. Gan, L. Dai, B. Xia, N. Zhan, D. Kapur and M. Chen: Interpolation synthesis for quadratic polynomial inequalities and combination with EUF. N. Olivetti and A. Tiwari (Eds.): IJCAR 2016, LNAI 9706, pp. 195–212, 2016.
J. Han, Z. Jin and B. Xia: Proving Inequalities and Solving Global Optimization Problems via Simplified CAD Projection. Journal of Symbolic Computation, vol. 72, pp. 206--230, 2016.
J. Han, L. Dai and B. Xia: Constructing Fewer Open Cells by GCD Computation in CAD Projection. In: Proc. ISSAC 2014, 240--247, ACM Press, 2014.
L. Dai, B. Xia and N. Zhan: Generating non-linear interpolants by semi-definite programming. In: N. Sharygina and H. Veith (Eds.): CAV 2013, LNCS 8044, pp. 364--380, Springer, Heidelberg (2013).