Project

General

Profile

Projects

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

  • Build Analyzer

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

  • BuildBase

    The base for the ant+ivy-based build system for Java 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....

  • Common Language ToolKit

    Base Eclipse plugins for integration of additional languages.

  • Coverage

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

  • CTESK

    UniTESK technology for C programming language

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

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

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

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

    • QEMU for ARMv8

      QEMU for ARMv8 is an open-source emulator for Aarch64 assembler programs based on QEMU. The emulator provides additional options for instruction logging and disassembling.

      The source package can be downloaded from the Files page....

    • MicroTESK for MIPS64

      MicroTESK for MIPS64 is a MicroTESK based instruction stream generator (ISG) aimed at functional verification of MIPS64 (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 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....

      • QEMU for RISC-V

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

    • 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: http://forge.ispras.ru/repo/xulrunner-eclipse/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 static verification framework that aims at automated checking of programs developed in the GNU C programming language against a variety of correctness rules using tools implementing such methods of thorough static analysis as Bounded Model Checking and Counterexample-Guided Abstraction Refinement....

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

    • C Instrumentation Framework

      C Instrumentation Framework is a user-friendly interface for Aspectator, a tool that implements aspect-oriented programming for the C programming language. Aspectator is included into the repository of C Instrumentation Framework as a submodule....

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

  • Local Support Project

    Local site support. Please follow Site Information And Rules.

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

  • Requality

    Requality is an 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 analyzing 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 extendible 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....

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

    UNDER CONSTRUCTION

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

  • UniTESK Reports

    Test trace processing tools and report generators

  • UniTestNG

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

  • VeriTool

    A simple utility intended for generation of C-Verilog synchronization components of a test system:

    • TestBench (a Verilog wrapper around the target module that launches a test scenario and generates a periodical clock pulse);
    • VPI-Mediator (a C API for accessing the target module's inputs and outputs);...
  • VerKer

    VerKer: Verification of Linux Kernel Library Functions

  • 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