Publications

Selected Papers

  • Denis Efremov, Mikhail Mandrykin, Alexey Khoroshilov
    Deductive Verification of Unmodified Linux Kernel Library Functions PDF
    8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II.

  • Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin, Eugene Novikov, Alexander Petrenko, Ilya Zakharov
    Configurable toolset for static verification of operating systems kernel modules PDF
    Programming and Computer Software, 2015, Volume 41, Number 1, pages 49-64.
    DOI: 10.1134/S0361768815010065

  • Alexey Khoroshilov,Vadim Mutilin, Ilya Zakharov
    Pattern-based environment modeling for static verification of Linux kernel modules
     Programming and Computer Software, 2015, Volume 41, Number 3, pages 183-195.
    DOI: 10.1134/S036176881503007X

  • E.A. Gerlits, A.V. Khoroshilov, V.V. Kuliamin, A.V. Maksimov, A.K. Petrenko, A.V. Tsyvarev
    Testing of Operating Systems (in Russian) PDF
    Proceedings of the Institute for System Programming of RAS, vol. 26, part 1, 2014, pp. 73-108.

  • Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin
    Introduction to CEGAR — Counter-Example Guided Abstraction Refinement (in Russian) PDF
    Proceedings of the Institute for System Programming of RAS, vol. 24, 2014, pp. 219-292.

  • Dirk Beyer, Alexander K. Petrenko
    Linux Driver Verification
    In T. Margaria and B. Steffen, editors, Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2012, Part II, Heraklion, Crete, October 15-18), LNCS 7610, pages 1-6, 2012. Springer-Verlag, Heidelberg.

  • Alexey Khoroshilov, Vadim Mutilin, Eugene Novikov
    Analysis of typical faults in Linux operating system drivers (in Russian) PDF
    Proceedings of the Institute for System Programming of RAS, vol. 22, 2012, pp. 349-372.

  • Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin, Eugene Novikov, Pavel 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

  • Alexey Khoroshilov, Vadim Mutilin, Eugene Novikov, Pavel Shved, Alexander Strakh
    Linux Driver Verification Architecture (in Russian) PDF
    Proceedings of the Institute for System Programming of RAS, vol. 20, 2011.

  • Alexey Khoroshilov, Vladimir Rubanov, Eugene Shatokhin
    Automated Formal Testing of C API Using T2C Framework
    Proceedings of 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Greece, 2008.

  • Denis Silakov, Vladimir Rubanov
    LSB Navigator – Online Reference for Linux Application Developers
    Proceedings of V Open Source Development Conference, Protva, 2008.

  • Vladimir Rubanov
    Standardization and Testing as Success Factors for Linux Security
    Proceedings of XVII Conference on «Methods and tools for informational security", St. Petersburg, 2008.

  • Alexey Khoroshilov, Vladimir Rubanov, Eugene Shatokhin
    T2C: Technology for Automated Development of Tests for Basic Functionality
    Proceedings of the Institute for System Programming of RAS, vol.I, part 2, 2008.

  • A. Grinevich, A. Khoroshilov, V. Kuliamin, D. Markovtsev, A. Petrenko, V. Rubanov
    Formal Methods in Industrial Software Standards Enforcement
    In I.Virbitskaite, A.Voronkov, eds. Proceedings of PSI'2006, LNCS 4378, pp.456-466.

  • Vladimir Rubanov
    Linux Standard Base (LSB): “Single Linux” Specification and Support Infrastructure
    Proceedings of the "Software Engineering Conference Russia 2007", November 2007.

  • Vladimir Rubanov
    Linux Standard Base (LSB): The Single Platform for Linux Applications (in Russian) PDF
    Proceedings of the I International Conference on "Standardizing Information Technology and Interoperability" (SITOP 2007), October 2007.

  • Alexey Khoroshilov
    Formal Specification of Interfaces as a Way to Improve Interoperability (in Russian) PDF
    Proceedings of the I International Conference on "Standardizing Information Technology and Interoperability" (SITOP 2007), October 2007.

  • Alexey Khoroshilov, Victor Kuliamin, Alexander Petrenko, Vladimir Rubanov
    Formalization of Interface Standards and Automatic Generation of Conformance Tests (in Russian) PDF
    Proceedings of Software Engineering Conference Russia (SECR 2006), November 2006.

  • Alexey Khoroshilov
    Linux Standard Base: Success Story? (in Russian)
    Proceedings of the Institute for System Programming of RAS, vol. 10, 2006.

  • Victor Kuliamin
    Formal Approaches for Testing Mathematical Functions (in Russian) PDF
    Proceedings of the Institute for System Programming of RAS, vol. 10, 2006.

  • A. Grinevich, A. Khoroshilov, V. Kuliamin, D. Markovtsev, A. Petrenko, V. Rubanov
    Using Formal Methods for Software Standards Enforcement (in Russian) PDF
    Proceedings of the Institute for System Programming of RAS, vol. 10, 2006.

  • Victor V. Kuliamin, Nickolay V. Pakoulin, and Alexander K. Petrenko
    Practical Approach to Specification and
    Conformance Testing of Distributed Network Applications     PDF
    Report at the 2-nd International Service Availability Symposium, Berlin, April 2005.

  • A.V. Barantsev, I.B. Burdonov, A.V. Demakov, A.V. Khoroshilov A.S. Kossatchev, V.V. Kuliamin, V.A. Omeltchenko, N.V. Pakoulin, A.K. Petrenko, S.V. Zelenov
    UniTESK Approach to Test Development: Achievements and Prospects PDF
    Proceedings of the Institute for System Programming of RAS, Vol. 5, 2004.

Press Releases and Presentations

Additional Information

Other publications and documents about UniTESK and corresponding tools can be found on the site http://unitesk.com/.

»