MicroTESK: MicroTESK 2.4.38 released

Added by Andrei Tatarnikov about 2 months ago

The new release contains the following changes:

  • Enhancements in the branch engine
  • Refactoring in the memory engine
  • New demo specifications and templates: Vmem ISA aimed to demonstrate the facilities of the memory engine
  • Changes in the nML language translator: special constructs to specify label-based instruction operands
  • Improvements in the simulator: correct handling of jump instructions
  • Improvements in the symbolic executor: correct SMT-formulae
  • Other general improvements

The MicroTESK distribution package can be downloaded from here:

QEMU for RISC-V: QEMU for RISC-V 0.2.1 released

Added by Sergey Smolov 4 months ago

The new release includes the following changes:

  • '-print-pte-addr' command line option (for more details see here)
  • '-trace-log' command line option (for more details see here)
  • logging for several kinds of events: instruction execution, GPR writes, memory loads/stores.

The source code can be downloaded from here

Klever: Klever 0.2

Added by Evgeny Novikov 5 months ago

Quite soon after the first release Klever 0.2 is available. Among all new features and bug fixes the most notable ones are the following:
  • Verification results processing, visualization and assessment:
    • Improving calculation and visualization of code coverage for particular verification tasks.
    • Calculation and visualization of code coverage split by correctness rule specifications for verification jobs or sub-jobs as a whole.
    • Switching to new functions for converting and comparing error traces by default as well as removing the outdated ones.
    • Fixes of processing, visualization and comparison of error traces for data races.
  • Verification back-ends:
    • Support for configuring verification back-ends.
    • Updating verification back-ends used by default.
    • Integration of Ultimate Automizer as an alternative verification back-end.
  • Verification tasks generation:
    • Ability to generate verification tasks consisting of several C source files.
    • Parallel generation of verification tasks and processing of verification results.
    • Reusing intermediate results obtained during verification tasks generation.
  • Support for installation and updates within OpenStack clouds.

Also available in: Atom