The MicroTESK framework will be presented at the University Booth exhibition and PhD Forum of the Design Automation Conference (DAC) - the premier conference for design and automation of electronic systems. The conference will take place on June 1-5 in San Francisco, CA, USA.

DAC offers outstanding training, education, exhibits and superb networking opportunities for designers, researchers, tool developers and vendors. The conference is sponsored by the Association for Computing Machinery (ACM), the Electronic Design Automation Consortium (EDA Consortium), and the Institute of Electrical and Electronics Engineers (IEEE), and is supported by ACM's Special Interest Group on Design. Read more...

C++TESK Testing ToolKit v1.0.24 has been released. The following things have been done.

• SGL (Simple Graph Library) has been implemented
• FSM test engine has been refactored
• Typed message fields have been supported
• PFSM (Probabilitic FSM) and FSM2 (FSM Pairs) test engines have been added

The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.

MicroTESK 2.0.2 has been released. The build contains the following changes:

• An ability to manualy specify initialization code was implemented
• The test templates library was improved
• Test template examples for ARM were updated
• Several bugs related to installation of MicroTESK were fixed
• Default test situations Random and Zero were provided

The main new feature of this update is support for viewing connection, memory and processor bindings in AADL Graphical Editor.
Now you can

• enable/disable showing all bindings of a particular kind using corresponding MASIW Toolbar buttons;
• enable/disable showing bindings for a particular component using context menu.

Also the update includes a number of bug fixes across various components of MASIW Framework.

We are happy to announce the first build of the MicroTESK 2.0 test program generator.

MicroTESK (Microprocessor TEsting and Specification Kit) is a reconfigurable framework for generating test programs for microprocessors and other programmable devices. The tool is customized for a specific instruction-set architecture with formal specifications in nML/Sim-nML language. Test programs are generated on a basis of test templates written in Ruby, which are abstract descriptions of test scenarios. Read more...

To generate test data, MicroTESK requires the Z3 solver be installed. See Installation Guide for more information.

The tool can be downloaded from the file page:
http://forge.ispras.ru/projects/microtesk/files

You are welcome to report bugs and leave your feedback at the main project site:
http://forge.ispras.ru/projects/microtesk

The MicroTESK tool will be presented at the University Booth exhibition of the DATE 2014 conference - one of the biggest European events for electronic system design and test. The conference & exhibition will take place on March 24-28 in Dresden, Germany.

DATE, the Design, Automation and Test Conference and Exhibition, is the unique European event bringing together researchers together researchers, users and vendors as well as specialists in design, test and manufacturing of electronic circuits and systems. The University Booth is a part of the DATE program. It is sponsored by the European Design and Automation Association, the EDA Consortium, the IEEE Council on EDA, ECSI, ACM SIGDA, and Russian Academy of Sciences. Read more...

The major feature of this release is a control groups based resource manager aimed to limit and to count resource consumption of verifiers. Linux control groups allow to perform very accurate measurements without any noticeable overhead. Other important changes are as follows:

• Support for automatic verification of modules of the Linux kernel in user-defined configurations, including different computer architectures.
• Addition of the new rule specification Locking and unlocking SDIO bus.
• Improvements in existing rule specifications: Module get/put and Block requests.
• Fixing all known segmentation faults in Aspectator.
• Switch to 2.7.2 version of BLAST verifier.
• Support of CBMC verifier as one of LDV Tools' back ends.
• Introducing a standalone error trace visualization tool.

Validation of LDV Tools 0.5 with different verifiers on 37 known bugs in the Linux kernel showed that:

• BLAST is able to detect 13 of them.
• CPAchecker is able to detect 11 of them.

In comparison with LDV Tools 0.4 6 known bugs were removed from the validation benchmark since they do not fit existing rule specifications, while 5 new known bugs were added to the benchmark (3 due to support of user-defined configurations, 1 due to addition of the new rule specification and 1 due to determining of an appropriate environment model). LDV Tools can detect two of those new bugs with help of BLAST verifier.

The source code repository can be browsed by v0.5 tag. To get and to install LDV Tools see instructions.

You may download sources and binaries on the Files page of the BLAST project. See also the original project page.

Release notes¶

This version only inroduces a few new options to support SV-COMP'14
competition rules:

• "-alias empty" to disable alias analysis ("-alias ''" is sometimes hard to specify)
• "-errorpathfile file" to print resulting (final) error trace to file
• "-propertyfile file" to read .prp property from the file specified

C++TESK Testing ToolKit v1.0.23 has been released. The following things have been done.

• MinGW is now supported
• Diagnostics subsystem has been improved
• Minor bugs have been corrected
• Support of configuration files has been improved
• Documentation has been moved to Wiki @ forge.ispras.ru/projects/cpptesk-toolkit

The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.

Fortress v0.3.0 (a redesigned version of Java Constraint Solver API) has been released.

The new release includes the following changes:

• the library was redesigned and renamed to Fortress
• the library was decomposed into a set of reusable packages (including data, expression, calculator, transform, solver)
• new classes for describing data were implemented (including a new bit vector implementation)
• a lot of refactoring has been done
• a number of bugs was fixed

The library can be downloaded from the page http://forge.ispras.ru/projects/solver-api/files