News

Linux Driver Verification: Google Summer of Code 2011 project was merged to master

Added by Evgeny Novikov almost 6 years ago

In frames of Google Summer of Code 2011 Ph.D. student Evgeny Novikov has successfully developed a project "User-friendly Interface for Linux Driver Verification Tools" with help of his mentor Alexey Khoroshilov for The Linux Foundation.

Within the given project a Knowledge Base support was developed. The Knowledge Base infrastructure allows users to keep results of unsafes analysis directly through the Statistics Server Web interface. Then these stored results are automatically applied to new uploaded unsafes in depend on different chosen comparison criteria. This significantly simplifies and speed ups the whole verification results analysis and makes the Linux Driver Verification project more attractive for end-users.

Also several minor issues of the Statistics Server related with usability and speed of page generation were resolved during Google Summer of Code 2011. One can see them here: #570, #1168, #1205, #1265, #1363, #1364, #1537, #1538

A Knowledge Base branch was merged to the master branch of the Linux Driver Verification project. It was successfully integrated with other tools, so stable Knowledge Base functionality is available beginning from 4ca264d.

We're going to continue develop and extend Knowledge Base infrastructure further. Keep in touch!

BLAST: BLAST 2.7 has been released

Added by Alexey Khoroshilov almost 6 years ago

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

Release notes

Analysis speedup

  • Fast and sound algorithm for alias analysis for pointers to structures without dereference depth limit enforced. Does not terminate on some programs with arbitrary-depth lists.
  • Add some normalization for better caching of postcondition requests.
  • Improved performance of lattice states merge.

New features

  • Re-animated function pointer support (-fp), which, however, doesn't distpatch correctly two or more functions aliased by the pointer.
  • Updated 64- and 32-bit versions of CSIsat allow you to analyze programs with as large numbers as your architecture supports.

Infrastructure improvements

  • Separated supported and unsupported options. Most recently added options has been made default.
  • Regression test suite may work in "competition" mode.

Bug fixes

  • Formulae caching in O(logN) useful blocks algorithm fixed (less FOCIinterface.SAT exceptions).

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.14 released

Added by Alexander Kamkin almost 6 years ago

C++TESK Testing ToolKit v1.0.14 has been released. A number of new features have been implemented.

  • New version of VeriTool.
  • Automatic catcher of unexpected reactions.
  • Macro CPPTESK_SET_DEBUG_LOGFILE(filename) to duplicate debug output into a file.
  • Basic Eclipse IDE plugin.

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

BLAST: BLAST 2.6 has been released

Added by Pavel Shved almost 6 years ago

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

Release notes

Analysis speedup

  • Speedup ranges from 8 times on small-sized programs to 30 times on medium-sized programs
  • Logarithmic algorithm for useful-blocks (significantly speedup of trace analysis)
  • Improved integration with SMT solvers
    • efficient string concatenation
    • caching of converted formulae
    • optimization of CVC3 options for BLAST use cases
  • Formulae normalization has been moved to solvers since solvers do it faster (option -skipnorm)
  • Alias analysis speedup
    • must-aliases are handled separately and faster than may-aliases (option -nomusts)
    • removed unnecessary debug prints from alias iteration (even a check for debug flag impacts performance significantly in hot places)
  • BLAST-specific tuning of OCaml virtual machine options (script "ocamltune")

Important bug fixes

  • Fixed unsound analysis when lattices are used (options -stop-sep and -merge) (Time of analysis has been increased by a factor of 1.5, but the inherent imprecision in lattices no longer makes BLAST miss bugs). See bug #330
  • bool-to-int casting in function calls fixed. See bug #334

Frontend

  • C frontend (CIL) uplift, fixes and workarounds (see -ignoredupfn and -nosserr options)
  • Some errors have been made warnings

New features

  • constrain stack depth to be analyzed; see options -fdepth, -important-attrs, and -inline-attrs
  • treat constant pointers as must aliases (see option -const)

Infrastructure improvements

  • Regression test suite improved
  • Got rid of non-free software (Simplify solver was replaced by CVC3, ditched unused Vampyre, FOCI, and CLPprover)

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.13 released

Added by Alexander Kamkin almost 6 years ago

C++TESK Testing ToolKit v1.0.13 has been released. The new features are as follows.

  • Example illustrating usage of C++TESK in couple with SystemVerilog (counter_sv)
  • Printing more information about MISSING, UNEXPECTED, and INCORRECT reactions
  • Installation guide in English
  • Support of 64-bit Linux systems

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

C++TESK Testing ToolKit: С++TESK web forums opened

Added by Alexander Kamkin almost 6 years ago

C++TESK web forums (one for Russian speakers and one for English speakers) opened today on http://forge.ispras.ru/projects/cpptesk-toolkit/boards.

We hope that forums will help both C++TESK users and developers. Users will be able to get useful information quickly and to exchange their experience, while developers will get immediate feedback from users.

Both forums are open for viewing; to post messages, an account is required. E-mail us to cpptesk-support [at] ispras.ru to get further information on how to get an account.

You are welcome to join the C++TESK community.

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.12 released

Added by Alexander Kamkin about 6 years ago

C++TESK Testing ToolKit v1.0.12 has been released. Several minor bugs have been fixed.

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

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.11 released

Added by Alexander Kamkin about 6 years ago

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

  • Simple heuristic to avoid getting caught in an endless loop during non-deterministic graph traversal has been implemented
  • Command line parameter --print-progress turning on the traversal progress printing has been added
  • Example cache_coherence has been included to demonstrate methods for state abstraction and non-deterministic graph traversal
  • One mistake in distributed test launching has been fixed
  • Scripts have been improved

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

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.10 released

Added by Alexander Kamkin about 6 years ago

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

  • Critical bug in the C++ test scenario wrapper (causing the last iteration to be missed) has been fixed
  • Debug print has been slightly corrected
  • New version of VeriTool has been attached

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

Local Support Project: Redmine 1.2.1, code review plugin 0.4.4 (5 comments)

Added by Alexey Demakov about 6 years ago

Redmine updated to 1.2.1.stable.6414.
Code review plugin updated: 0.4.0 -> 0.4.4
Please report if you find any problems.

1 ... 23 24 25 26 27 ... 29 (241-250/282)

Also available in: Atom