Alexey has graduated from Computer Sciences Department of the Lomonosov's Moscow State University with honour in 2001. He received a Ph.D. in Computer Sciences in 2006 on the Formal Specification and Testing of Asynchronous Systems (under supervision of prof. Alexander Petrenko).

Alexey works for the Institute for System Programming of the Russian Academy of Sciences (ISPRAS) since 1999. His research interest includes formal methods for software and hardware systems, model based testing, verification of operating systems and design of safety critical embedded systems. Alexey was the lead architect of the LSB Infrastructure program run jointly by ISPRAS and Linux Foundation. He is a director of the Linux Verification Center of ISPRAS, where a number of verification techniques are developed and applied to Linux kernel.

Selected publications: (see also Google Scholar)

1. Alexey Grinevich, Alexey Khoroshilov, Victor Kuliamin, Denis Markovtsev, Alexander Petrenko, Vladimir Rubanov. “Formal Methods in Industrial Software Standards Enforcement”, PSI 2006, LNCS Vol. 4378, 2006, pp. 446-455.
2. N.V. Pakulin, A.V. Khoroshilov "Development of formal models and conformance testing for systems with asynchronous interfaces and telecommunications protocols" // Programming and Computer Software. 2007. Т. 33. № 6. С. 316-335.
3. Alexey V. Khoroshilov, Vladimir V. Rubanov and Eugene A. Shatokhin. «Automated Formal Testing of C API Using T2C Framework» // In Proceedings of the Third International Symposium «Leveraging Applications of Formal Methods, Verification and Validation» (ISoLA 2008), Porto Sani, Greece, October 13-15, 2008. pp 56-70.
4. A. Khoroshilov, V. Mutilin, A. Petrenko, V. Zakharov. “Establishing Linux Driver Verification Process”, in A. Pnueli, I. Virbitskaite, A. Voronkov, eds. Perspectives of Systems Informatics, LNCS 5947:165-176, Proceedings of PSI-2009, Novosibirsk, Russia, June 15-19, 2009.
5. A. Ponomarenko, V. Rubanov, A. Khoroshilov. "A system for backward binary compatibility analysis of shared libraries in Linux", Proceedings of 5th Software Engineering Conference in Russia (CEE-SECR), 2009, pp.25-31.
6. A. Khoroshilov, V. Kuliamin, A. Petrenko, O. Petrenko, V. Rubanov. “Building open learning environment for software engineering students” in "Free and Open Source Software for E-Learning: Issues, Successes and Challenges" / Betul Ozkan Czerkawski, editor, ISBN 978-1-61520-917-0, pp. 110-119, Information Science Reference, New York, 2011.
7. Alexey Khoroshilov, Igor Koverninskiy, Alexander Petrenko and Alexender Ugnenko. "Integrating AADL-based Tool Chain into Existing Industrial Processes". // In Proceedings of 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS-2011), pp. 367-371, ISBN: 978-1-61284-853-2, Las Vegas, USA, April 27-29, 2011.
8. D. V. Silakov, A. V. Khoroshilov «Ensuring portability of software» //Programming and Computer Software, 2011, Volume 37, Number 1, pp. 41-47.
9. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A., Towards an Open Framework for C Verification Tools Benchmarking. // In Proceedings of the Eighth International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» (PSI 2011), 82-91, Novosibirsk, Russia, June 27 - July 1, 2011.
10. Y. Gerlits, A. Khoroshilov. "Model-Based Testing of Safety Critical Real-Time Control Logic Software" // In Proceedings of the Seventh Workshop on Model-Based Testing (MBT 2012), Tallin, Estonia, March 25, 2012.
11. M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. V. Khoroshilov, and P. E. Shved "Using Linux Device Drivers for Static Verification Tools Benchmarking" //Programming and Computer Software, 2012, Volume 38, Number 5, Pages 245-256. DOI: 10.1134/S0361768812050039
12. Alexey Khoroshilov, Vadim Mutilin, Eugene Novikov. "Analysis of typical faults in Linux operating system drivers". Proceedings of the Institute for System Programming of RAS, vol. 22, 2012, pp. 349-372.
13. Khoroshilov, A., Albitskiy, D., Koverninskiy, I., Olshanskiy, M., Petrenko, A., Ugnenko, A., "AADL-Based Toolset for IMA System Design and Integration", SAE Int. J. Aerosp. 5(2):2012, doi:10.4271/2012-01-2146.
14. Petr Devyanin, Alexey Khoroshilov, Victor Kuliamin, Alexander Petrenko, Ilya Shchepetkov "Formal Verification of OS Security Model with Alloy and Event-B" // In A. Yamine and K.-D. Schewe, eds. Abstract State Machines, Alloy, B, TLA, VDM, and Z, LNCS 8477:309-313, Proceedings of ABZ-2014, Toulouse, France, June 2-6, 2014. ISBN: 978-3-662-43651-6, DOI: 10.1007/978-3-662-43652-3_30
15. Alexey Khoroshilov, Vadim Mutilin, Evgeny Novikov, Ilja Zakharov "Modeling Environment for Static Verification of Linux Kernel Modules". In A. Voronkov, I. Virbitskaite. Lecture Notes in Computer Sciences #8974 "PERSPECTIVES OF SYSTEM INFORMATICS", PSI 2014, pp. 400-414, Springer Berlin Heidelberg.
16. D.Buzdalov, A.Khoroshilov. "A discrete-event simulator for early validation of avionics systems". Proceedings of the First International Workshop on Architecture Centric Virtual Integration - ACVI 2014, Valencia, Spain, September 29, 2014. CEUR‑WS Vol-1233, pp.28-38.
17. A. V. Khoroshilov, M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. K. Petrenko, and I. S. Zakharov "Configurable toolset for static verification of operating systems kernel modules" //Programming and Computer Software, 2015, Volume 41, Number 1, Pages 49-64.
18. A. V. Khoroshilov, V. S. Mutilin, I. S. Zakharov "Pattern-based environment modeling for static verification of Linux kernel modules" //Programming and Computer Software, 2015, Volume 41, Number 3, Pages 183-195.
19. M. U. Mandrykin, A. V. Khoroshilov "High-Level Memory Model with Low-Level Pointer Cast Support for Jessie Intermediate Language" //Programming and Computer Software, 2015, Volume 41, Number 4, Pages 197-207.
20. Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya V. Shchepetkov "Using Refinement in Formal Development of OS Security Model". In Lecture Notes in Computer Sciences #9609 "Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference", pp. 107-115, Springer International Publishing.
21. M.U. Mandrykin, A.V. Khoroshilov "Region analysis for deductive verification of C programs" //Programming and Computer Software, 2016, Volume 42, Number 5, Pages 257-278.
22. Pavel Andrianov, Vadim Mutilin, Alexey Khoroshilov "Predicate abstraction based configurable method for data race detection in Linux kernel". // In Communications in Computer and Information Science #779 "TMPA 2017: Tools and Methods of Program Analysis", pp. 11-23.
23. Mikhail Mandrykin, Alexey Khoroshilov "A Memory Model for Deductively Verifying Linux Kernel Modules". In Lecture Notes in Computer Sciences #10742 "Perspectives of System Informatics: 11th International Andrei P. Ershov Informatics Conference", pp. 256-275.
24. Denis Efremov, Mikhail Mandrykin, Alexey Khoroshilov. Deductive Verification of Unmodified Linux Kernel Library Functions. 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II. 216-234. 10.1007/978-3-030-03421-4_15.
25. Cheptsov V., Alexey Khoroshilov A. Dynamic Analysis of ARINC 653 RTOS with LLVM // IEEE The Proceedings of the 2018 Ivannikov ISPRAS Open Conference (ISPRAS-2018) 2018. P. 9-15.
26. Kildishev D.S., Khoroshilov A.V. Formalizing metamodel of Requirements Management System. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 5, 2018, pp. 163-176.
27. P.N. Devyanin, D.V. Efremov, V.V. Kuliamin, A.K. Petrenko, A.V. Khoroshilov, I.V. SHchepetkov. Operating system security policy modeling and verification. (In Russian) Goryachaya liniya – Telecom Moscow, 2019.