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
Расширяемый инструментарий для анализа процесса сборки программных проектов.
Основная область применения на начальном этапе - извлечение информации о структуре Си программ с целью их последующего анализа.
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....
- С++TESK Development Environment
Eclipse-based C++TESK integrated development environment.
- C Instrumentation Framework
- Common Language ToolKit
Base Eclipse plugins for integration of additional languages.
Library managing hierarchical coverage structures and annotated Java descriptions for them.
- 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.
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....
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 for Plasma
A MicroTESK-based test program generator (instruction stream generator) for the Plasma microprocessor.
- MicroTESK for RISC-V
- 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 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 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....
A C library for high-precision floating-point computations.
The library is designed to be compatible with a standard libm library. Just change the
-lmcompiler option to
-lunifloat -fno-builtinwhen 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 (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 (
mainfunction) by a valid execution....
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.
- 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 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 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....
Semantic Testing Kit
Syntax Testing Kit
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....
- UniTESK Reports
Test trace processing tools and report generators
The library for testing of translators (input files -> output files) using TestNG.
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: Verification of Linux Kernel Library Functions
- MASIW Framework
- 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