SPARK: A Framework for Multi-Scale Agent-Based Biomedical Modeling. - Alexey Solovyev; Maxim Mikheev; Leming Zhou; Joyeeta Dutta-Moscato; Cordelia Ziraldo; Gary An; Yoram Vodovotz; Qi Mi (Int. J. Agent Technol. Syst., 2010)

Efficient Formal Verification of Bounds of Linear Programs. - Alexey Solovyev; Thomas C. Hales (Calculemus/MKM, 2011)

A Machine-Checked Proof of the Odd Order Theorem. - Georges Gonthier; Andrea Asperti; Jeremy Avigad; Yves Bertot; Cyril Cohen; François Garillot; Stéphane Le Roux 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations. - Alexey Solovyev; Thomas C. Hales (NASA Formal Methods, 2013)

Hybrid Equation/Agent-Based Model of Ischemia-Induced Hyperemia and Pressure Ulcer Formation Predicts Greater Propensity to Ulcerate in Subjects with Spinal Cord Injury. - Alexey Solovyev; Qi Mi; Yi-Ting Tzen; David M. Brienza; Yoram Vodovotz (PLoS Comput. Biol., 2013)

Efficient search for inputs causing high floating-point errors. - Wei-Fan Chiang; Ganesh Gopalakrishnan; Zvonimir Rakamaric; Alexey Solovyev (PPoPP, 2014)

Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. - Alexey Solovyev; Charles Jacobsen; Zvonimir Rakamaric; Ganesh Gopalakrishnan (FM, 2015)

A formal proof of the Kepler conjecture. - Thomas C. Hales; Mark Adams; Gertrud Bauer; Dat Tat Dang; John Harrison 001; Truong Le Hoang; Cezary Kaliszyk; Victor Magron; Sean McLaughlin; Thang Tat Nguyen; Truong Quang Nguyen; Tobias Nipkow; et al. (CoRR, 2015)

A Parameterized Floating-Point Formalizaton in HOL Light. - Charles Jacobsen; Alexey Solovyev; Ganesh Gopalakrishnan (NSV, 2015)

A Computational, Tissue-Realistic Model of Pressure Ulcer Formation in Individuals with Spinal Cord Injury. - Cordelia Ziraldo; Alexey Solovyev; Ana Allegretti; Shilpa Krishnan; M. Kristi Henzel; Gwendolyn A. Sowa; David M. Brienza; Gary An; Qi Mi; Yoram Vodovotz (PLoS Comput. Biol., 2015)

Moving the Needle on Rigorous Floating-Point Precision Tuning. - Marek S. Baranowski; Ian Briggs; Wei-Fan Chiang; Ganesh Gopalakrishnan; Zvonimir Rakamaric; Alexey Solovyev (AFM@NFM, 2017)

Rigorous floating-point mixed-precision tuning. - Wei-Fan Chiang; Mark Baranowski; Ian Briggs; Alexey Solovyev; Ganesh Gopalakrishnan; Zvonimir Rakamaric (POPL, 2017)

Rigorous Estimation of Floating-Point Round-Off Errors with Symbolic Taylor Expansions. - Alexey Solovyev; Marek S. Baranowski; Ian Briggs; Charles Jacobsen; Zvonimir Rakamaric; Ganesh Gopalakrishnan (ACM Trans. Program. Lang. Syst., 2019)

Rigorous Error Analysis for Logarithmic Number Systems. - Thanh Son Nguyen; Alexey Solovyev; Ganesh Gopalakrishnan (CoRR, 2024)

Rigorous Error Analysis for Logarithmic Number Systems. - Thanh Son Nguyen; Alexey Solovyev; Mark G. Arnold; Ganesh Gopalakrishnan (ARITH, 2025)