Welcome to the ISP RAS open-source projects!
At the moment this system presents selected projects being developed by the
Software Engineering department.

We focus on advanced R&D in the area of software and hardware testing and
verification methods, tools and technologies. We work both on fundamental
R&D funded by the Russian Academy of Sciences and on industrial R&D projects
funded by our partners such as Linux Foundation, Intel, Microsoft, Nokia and

Follow Site Information And Rules please.

IMPORTANT: Permanently authenticating with Git repositories

IMPORTANT: How to create repository.

IMPORTANT: Additional services.

Help and support can be obtained in Local Support Project.

Latest news

QEMU for RISC-V: QEMU for RISC-V v0.1.1 released
QEMU for RISC-V v0.1.1 has been released.
Added by Sergey Smolov 13 days ago

Klever: Klever 0.2
Added by Evgeny Novikov about 1 month ago

QEMU for ARMv8: QEMU for ARMv8 0.1.10 released
QEMU for ARMv8 0.1.10 has been released.
Added by Sergey Smolov about 1 month ago

MicroTESK: MicroTESK 2.4.37 released
MicroTESK 2.4.37 has been released.
Added by Andrei Tatarnikov 2 months ago

Trace Matcher: Trace Matcher 0.1.8 released
Trace Matcher 0.1.8 has been released.
Added by Sergey Smolov 2 months ago

View all news

Latest projects

  • QEMU for RISC-V (11/02/2017 02:47 pm)

    QEMU for RISC-V is an open-source emulator for RISC-V assembler programs based on QEMU.

  • Crude_slicer (10/31/2017 03:18 pm)

    Prototype slicer for preprocessing reachability verification tasks

    Reachability slicer based on context-sensitive flow-insensitive separation analysis with typed polymorphic regions and dependency analysis with transitive closures. Intended to be used with a reachability verifier e.g. CPAchecker, Ultimate Automizer, CBMC, for verification tasks prepared from Linux device drivers. The slicing is performed modulo termination. So the slicer works under assumption that all the code (except for explicitly specified functions) necessary terminates and thus can be removed if it doesn't influence reachability....

  • VerKer (05/09/2017 10:51 pm)

    VerKer: Verification of Linux Kernel Library Functions

  • Build Analyzer (04/19/2017 11:47 am)

    Расширяемый инструментарий для анализа процесса сборки программных проектов.
    Основная область применения на начальном этапе - извлечение информации о структуре Си программ с целью их последующего анализа.

  • Examples of behavioral AADL models (02/10/2017 09:03 pm)

    This is a project for AADL models intended to show different approaches to behaviour modelling with AADL and analyzing of these behaviours using MASIW, especially with simulation.