Apply Clear

  • Aspectrace

    Aspect-oriented Tracing facility.

    Provides extensible trace format specification and framework for creating traces, analyzing them and creating modularizable reports. Supports pluggable independent libraries of message types (each library presents its own "aspect"), facilitates merging and linking data from different aspects and converting it into mutually-linked report entities....

  • AstraVer Toolset

    Набор инструментов для верификации моделей политик безопасности и их реализаций в ответственных системах.

    Набор инструментов в настоящий момент состоит из двух частей:
    • Deductive Verification Tools for Linux Kernel

      The project aims to improve open source deductive verification tools, so they can be used to prove properties of Linux kernel code. Our efforts are based on 'Frama-C - Jessie plugin - Why3' tool chain.

      See build instructions in wiki.

      • Verification Tool Supports

        В данном репозитории собран ряд утилит для изучения исходных кодов модуля ядра Linux и для работы с ними.

        Описание утилит смотрите на wiki.

    • Дополнительные материалы к монографии

      Дополнительные материалы к монографии "Моделирование и верификация политик безопасности управления доступом в операционных системах".

    • Инструменты дедуктивной верификации моделей политик безопасности

      Набор инструментов предназначен для верификации моделей политик безопасности в соответствии с требованиями с ГОСТ Р ИСО/МЭК 15408-3 [1] в части семейства требований доверия «Моделирование политики безопасности» (ADV_SPM).

      В настойщий момент разработка моделей ведётся на формальном языке Event-B. Для разработки и верификации моделей используется инструментальная среда, основанная на платформе Rodin, разрабатываемой под свободной лицензией ETH Zurich, Systerel, Clearsy, University of Newcastle и University of Southampton....

  • Build Analyzer

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

  • BuildBase

    Gradle-based build system for Eclipse projects

  • C++TESK Testing ToolKit

    C++TESK Testing ToolKit is an open-source C++ based toolkit intended for automated functional testing of software components (mostly in C/C++) and RTL (HDL) models of digital hardware (in Verilog and VHDL). The main part of the toolkit is a library of C++ classes and macros that define facilities for constructing formal specifications (reference models), adapters of components under test, test scenarios and test coverage metrics. Basing on C++ descriptions provided by a user, a test system is compiled. It allows automatically generating and applying sequences of stimuli to the component under test, checking correctness of its reactions and collecting statistics on test execution. Besides the basic library, the toolkit includes a report generator, means for parallelizing test execution on computer clusters, and Eclipse-based IDE....

  • Castle

    Castle (Control flow & Abstract Syntax Tree Library, Etc.) is a simple library for developing translators and code generators.

    Licensing and Distribution

    The Castle package is distributed under the Apache License, Version 2.0, which implies the freedom to use the software for any purpose (to distribute it, to modify it and to distribute modified versions of the software) under the terms of the license, but requires preservation of the copyright notice and disclaimer....

  • C Instrumentation Framework

    C Instrumentation Framework is a tool that implements aspect-oriented programming for the C programming language. You can find more information about it in paper An approach to implementation of aspect-oriented programming for C.

    CIF documentation:

  • Clade

    Clade is a tool for intercepting build commands (stuff like compilation, linking, mv, rm, and all other commands that are executed during build). Intercepted commands can be parsed (to search for input and output files, and options) and then used for various purposes:...

  • Common Language ToolKit

    Base Eclipse plugins for integration of additional languages.

  • Coverage

    Library managing hierarchical coverage structures and annotated Java descriptions for them.


    UniTESK technology for C programming language

    CTESK depends on UniTESK Reports for test trace processing and report generation.

  • Ductilejur

    Прототип архитектуры инструмента моделирования, основанной на использовании и композиции полиморфного строго типизированного чисто-функционального кода

    Работа поддержана грантом РФФИ №17-01-00504

    Публикации, связанные с проектом

  • Formal Methods

    Курс "Формальные методы верификации программ" / "Верификация ПО. Часть 2" (читается с осени 2013 года).

  • Fortress

    Fortress (FORmula TRanslation, Evaluation and Symbolic Simplification), former JCSA (Java Constraint Solver API), is an open-source and extendable Java library providing facilities for manipulation with formulae (terms and constraints). The library allows creating formulae (in the form of syntax trees), translating them into external formats (programming languages, XML, SMT-LIB, etc.), evaluating them and doing symbolic simplification. It also supports constraint solving using built-in solvers as well as external ones (like Yices, Z3, CVC4, Boolector, etc.). For more information, read Wiki....

  • Java 5 frontend

    Java 5 frontend consists of syntax checker (parser) building AST and semantic checker verifying static semantics.

    Note: Semantic checker implementation is in JavaTESK project as a part of semantic checker for the extension of Java language. It will be extracted when we have enough resources....

  • Java Object Graph Snapshotter

    JOGS provides facilities for flexible processing of graphs of Java objects.
    It's capable of "remembering", "restoring", and "comparing" state(s) of the whole object graph without
    creating new instances of classes involved in the graph structure.

  • Java SoftFloat

    Java SoftFloat is a Java implementation of the Berkeley SoftFloat library, a free, high-quality software implementation of binary floating-point that conforms to the IEEE Standard for Floating-Point Arithmetic. As the original version, Java SoftFloat fully implements four floating-point formats: 32-bit single-precision, 64-bit double-precision, 80-bit double-extended-precision, and 128-bit quadruple-precision....

  • JavaTESK

    UniTESK technology for Java programming language

    JavaTESK depends on UniTESK Reports for test trace processing and report generation.

  • Kartographer

    Kartographer is designed to build a call graph of the Linux kernel for a given configuration. It also collects information about macros, function pointers, object and source files.

    Besides the Linux kernel, Kartographer can be used in other projects written in C....

  • MicroTESK

    MicroTESK is a reconfigurable (retargetable and extendable) model-based test program generator (TPG) for microprocessors and other programmable devices (such kind of tools are also called instruction stream generators or ISG). The generator is customized with the help of instruction-set architecture (ISA) specifications and configuration files, which describe parameters of the microprocessor subsystems (pipeline, memory and others). The suggested approach eases the model development and makes it possible to apply the model-based testing in the early design stages when the microprocessor architecture is frequently modified....

    • MicroTESK Documentation

      This project contains MicroTESK documentation, including the installation instruction, the user guide, and the development guide.

    • MicroTESK for ARM Demo

      MicroTESK for ARM Demo is a demo-version of the MicroTESK based instruction stream generator (ISG) aimed at functional verification of ARM microprocessors.

    • MicroTESK for MIPS

      MicroTESK for MIPS is a MicroTESK based instruction stream generator (ISG) aimed at functional verification of MIPS (Release 6) microprocessors.

      The package can be downloaded from the Files page. Here is an Installation Guide....

    • MicroTESK for Plasma

      A MicroTESK-based test program generator (instruction stream generator) for the Plasma microprocessor.

    • MicroTESK for PowerPC

      MicroTESK for PowerPC is a MicroTESK based instruction stream generator (ISG) aimed at function verification of PowerPC microprocessors. More precisely, this research project focuses on the PowerISA v.2.06 ISA and the e500mc CPU (NXP Semiconductors)....

    • MicroTESK for RISC-V

      MicroTESK for RISC-V is a MicroTESK based instruction stream generator (ISG) aimed at functional verification of RISC-V microprocessors.

      The package can be downloaded from the Files page. Here is an Installation Guide....

    • MicroTESK Training Course

      Курс предназначен для студентов старших курсов, специализирующихся в области проектирования и верификации микропроцессоров. Цели курса — познакомить слушателей с методами спецификации микропроцессоров и методами генерации тестовых программ, а также выработать соответствующие практические навыки. Основу курса составляют практичекие занятия, посвященные спецификации инструкций и созданию автоматизированных генераторов тестовых программ для MIPS-совместимого микропроцессора. Практикум основан на языке спецификации nML (Sim-nML) и инструменте создания генераторов тестовых программ MicroTESK....

    • Trace Matcher

      Utilities for microprocessor execution traces matching.

  • Mozilla XULRunner Eclipse plug-in

    Mozilla XULRunner packaged as Eclipse-plugin

    Update site:

  • Race Hound

    Data Race Detector for Linux Kernel

  • KEDR

    KEDR is an extensible system for dynamic (runtime and post factum) analysis and verification of Linux kernel modules. KEDR tools operate on the modules chosen by the user and can perform function call monitoring, fault simulation, memory leak detection and more....

  • Klever

    Klever is a software verification framework that aims at automated checking of programs developed in the GNU C programming language against a variety of requirements using software model checkers (automatic software verification tools) implementing such methods of thorough static analysis as Bounded Model Checking and Counterexample-Guided Abstraction Refinement. Software model checking allows finding faults that can be hardly detected by other software quality assurance techniques like code review, testing and static analysis. In addition, it is capable to prove formal correctness of programs checked against particular requirements under certain assumptions....

  • libUniFloat

    A C library for high-precision floating-point computations.

    The library is designed to be compatible with a standard libm library. Just change the -lm compiler option to -lunifloat -fno-builtin when building your application and you'll get high-precision versions of trigonometric (sin, tan, ...), bessel (jn, yn, ...) and other functions declared in the standard math.h header file....

  • Linux Driver Verification

    This page is a development portal of the Linux Driver Verification project. The aim of LDV is to build a comprehensive application suite for static verification of source code of Linux device drivers, and monitoring their quality....

    • BLAST

      BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution....

    • Crude_slicer

      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....

    • Linux Kernel Safety RuleDB

      The project aimed to collect and prioritize rules of correct usage of Linux kernel core API by kernel-space loadable modules.

  • Технологический центр исследования безопасности ядра Linux

    Материалы, посвящённые созданию Технологического центра исследования безопасности ядра Linux.

    По всем вопросам пишите:

  • Local Support Project

    Local site support. Please follow Site Information And Rules.

  • memconfigcheck

    Данный проект посвящен задаче верификации разделения ресурсов в операционных системах для встроенных систем.
    Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта №16-01-00356.

    Научный отчет...

  • Model Checking

    Курс "Верификация моделей программ" для студентов 1-ого курса магистратуры ВМиК (читается с февраля 2016 года).

  • Native Java Launcher

    NJL (Native Java Launcher) is platform-dependent launcher for Java applications.
    This launcher is written in C and can be ported to many platforms.
    NJL reads Java classpath and command-line options from configuration file to make Java application command-line much simpler....

  • Imperative HOL examples

    Preliminary manual translations of verified C/ACSL functions into Imperative HOL

  • TSMT: Tools for bounded E-Matching

    A set of Isabelle proof methods and commands that facilitates the use of relatively complete decision procedures (e.g. SMT solvers and paramodulation-based provers) with deterministic quantifier instantiation based on bounded E-matching. More about TSMT is explained in the TSMT Tutorial....

  • QEMU4V

    QEMU4V ("QEMU for Verification") is an open source emulator for assembler programs that is based on QEMU project. The tool performs emulation for programs of several hardware architectures and provides some features (tracing, etc.) for system verification of microprocessors....

  • Requality

    Requality is an open source Eclipse-based Requirements Management Tool that supports both development of requirements from scratch as well as recreation of a hierarchy of requirements from existing documents. Requality keeps linkage between a requirement and fragments of documents that became a source for the requirement that makes Requality very attractive for reverse engineering of requirements. Another important feature of the tool is a support for Requirements-based Test Purpose Design....

  • Retrascope

    Retrascope is a toolkit for Reverse Engineering, visualization and TRAnsformation of digital hardware designs described in such HDLs (hardware description languages) as Verilog and VHDL. The toolkit allows analysing HDL descriptions, reconstructing and visualization of the underlying models (extended finite state machines, EFSMs) and using the derived models for test generation, property checking and other tasks. Retrascope is organized as an extendable framework with the ability to add new types of models as well as tools for their analysis and transformation. The primary application domain of the toolkit is functional verification of hardware at the unit level....

  • Runtime Verification

    Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы.

  • SemaTESK

    Semantic Testing Kit

  • SynTESK

    Syntax Testing Kit

  • TestBase

    TestBase is a knowledge base used for test data generation. It stores data constraints and generators and handles user queries to build test data providers.


    Licensing and Distribution

    The TestBase package is distributed under the Apache License, Version 2.0, which implies the freedom to use the software for any purpose (to distribute it, to modify it and to distribute modified versions of the software) under the terms of the license, but requires preservation of the copyright notice and disclaimer....

  • Track Finding Tools for NICA MPD

    Experimental track finding tools for the MPD detector of the NICA project.

  • UniTESK Reports

    Test trace processing tools and report generators

  • UniTestNG

    The library for testing of translators (input files -> output files) using TestNG.

  • Verilog Translator

    Verilog Translator (VeriTrans) is an ANTLR-based Verilog front-end in couple with some back-ends.

    Licensing and Distribution

    The VeriTrans package is distributed under the Apache License, Version 2.0, which implies the freedom to use the software for any purpose (to distribute it, to modify it and to distribute modified versions of the software) under the terms of the license, but requires preservation of the copyright notice and disclaimer....

  • Veritool

    A simple utility aimed at generating C-Verilog synchronization components of a test environment:

    table=. {font-style:italic; font-weight:bold; background:#dddddd}. |<. Component |<. Description | |<. Testbench |<. a Verilog wrapper around the DUT that generates a clock signal, launches a test scenario, and does cycle-by-cycle synchronization w/ the test environment |...

  • VerKer - Verification of Linux Kernel Library Functions

    VerKer: Verification of Linux Kernel Library Functions

    See more details in our wiki.

  • MASIW Framework

    MASIW Framework is an open source Eclipse-based IDE for development and analysis of AADL models. It is developed by ISPRAS in cooperation with GosNIIAS.

    The main features of the toolkit includes:
    • textual and graphical editors for AADL model;...
    • Examples of behavioral AADL models

      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.

  • Материалы конференций

    Выкладываются электронные материалы конференций и семинаров, в работе которых мы участвовали

  • Тесты с использованием моделей на базе Summer

    Проекты автоматизированного тестирования программных интерфейсов с использованием моделей. В качестве фреймворка для тестов используется библиотека Summer.

Also available in: Atom