Alexey Solovyev

Alexey Solovyev

University of Utah, School of Computing
50 S. Central Campus Drive Rm 3190
Salt Lake City, Utah 84112

alexey (dot) solovyev (AT)


I am a postdoctoral researcher in the School of Computing at the University of Utah. I am a member of Prof. Ganesh Gopalakrishnan's Gauss Group.

I obtained my PhD in mathematics from the University of Pittsburgh.

Curriculum Vitae

PhD Thesis Formal Computations and Methods


10. Chiang, W.; Gopalakrishnan, G.; Rakamaric, Z.; Solovyev, A. Efficient Search for Inputs Causing High Floating-point Errors. PPoPP 2014,
9. Gonthier, G.; Asperti, A.; Avigad, J.; Bertot, Y.; Cohen, C.; Garillot, F.; Roux, S.; Mahboubi, A.; O'Connor, R.; Biha, S.; Pasca, I.; Rideau, L.; Solovyev, A.; Tassi, E.; Thery, L. A Machine-Checked Proof of the Odd Order Theorem. LNCS, ITP 2013 2013, 7998, 163–179. [link]
8. Solovyev, A.; Hales, T. Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations. LNCS, NFM 2013 2013, 7871, 383–397. [link]
7. Solovyev, A.; Mi, Q.; Tzen, Y.; Brienza, D.; Vodovotz, Y. Hybrid Equation/Agent-Based Model of Ischemia-induced Hyperemia and Pressure Ulcer Formation Predicts Greater Propensity to Ulcerate in Subjects with Spinal Cord Injury. PLoS Comput Biol 2013, [link]
6. Solovyev, A.; Hales, T. Efficient formal verification of bounds of linear programs. LNCS, CICM 2011 2011, 6824, 123–132. [link]
5. Mi, Q.; Constantine, G.; Ziraldo, C.; Solovyev, A.; Torres, A.; Namas, R.; Bentley, T.; Billiar, T.R.; Zamora, R.; Puyana, J.C.; Vodovotz, Y. A dynamic view of trauma/hemorrhage-induced inflammation in mice: Principal drivers and networks. PLoS ONE 2011, [link]
4. Solovyev, A.; Mikheev, M.; Zhou, L.; Dutta-Moscato, J.; Ziraldo, C.; An, G.; Vodovotz, Y.; Mi, Q. SPARK: A Framework for Multi-Scale Agent-based Biomedical Modeling. International Journal of Agent Technologies and Systems 2010, 2, 18–30. [link]
3. Mikheev, M.; Solovyev, A.; Maltsev, A.; Bartels, J.; Chang, S.; Mi, Q.; Vodovotz, Y. A parallel implementation of an agent-based modeling platform with application in modeling calcium releases in cardiomyocytes. Journal of Critical Care 2009, 24, [link]
2. Garnaev, A.; Solovyev, A. An Investment Allocation Game with a Cost. Int. J. Math. Game Theory and Algebra 2006, 15, 221–229.
1. Garnaev, A.; Solovyev, A. On a Two Department Multi-Stage Game (in Russian). Vestnik St. Petersburg University, Seria 10, Applied Mathematics 2005, 3–12.



A cross-platform free software for multi-scale Agent-based modeling.

Authors: Alexey Solovyev, Qi Mi, Maxim Mikheev


A programming language for rapid development of Agent-based models in SPARK.

Author: Alexey Solovyev


A formal proof of the Kepler conjecture.

Author: Thomas Hales

SSReflect/HOL Light

An implementation of the SSReflect proof language in HOL Light.

Author: Alexey Solovyev

Formal Verification of Nonlinear Inequalities

A tool for formal verification of multivariate nonlinear inequalities in HOL Light.

Author: Alexey Solovyev

Guided Random Testing for Floating-point Error Estimation

Author: Wei-Fan Chiang