The new release contains the following changes:
- New SmtKeyword class for SMT-LIBv2 keywords
- Print user data for unsupported operation
- SmtTextSolver: always parse model for array values
- Other bug fixes and code improvements
The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files
Redmine 4.0.3
Уважаемые коллеги!
Redmine обновился до версии 4.0.3, которая использует rails 5.2.3
В rails предыдущих версий найдена критическая уязвимость.
Нет никаких свидетельств, что уязвимость эксплуатировалась на этом сайте.
К сожалению, все плагины требуют доработки, поэтому пока отключены.
The new release contains the following changes:
- Support for block-level register allocation constraints
- Changes in the register allocation engine
- MMU plugin: structures' fields are listed from upper to lower bits
- Bug fixes and code improvements
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
The new release includes the following bugfix:
- Aarch64: increase size of internal string buffer
The source code can be downloaded from here
The new release is based on
QEMU 3.1.0 and includes the following features:
- Basic support for PowerPC programs emulation
- Trace generation for PowerPC (32bit) programs
The complete list of resolved issues is available here
The source code can be downloaded from here
The new release contains the following changes:
- Support for separate-file sections (useful for boot generation)
- Support for the 'decode' attribute of nML primitives (experimental)
- Decoder generator: enabling bit selection for non-immediate arguments
- Bug fixes and code improvements
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
The new release includes the following features:
- Trace generation for MIPS (MIPS64) programs
The complete list of resolved issues is available here
The source code can be downloaded from here
We are happy to announce that Klever 2.0 is released!
Klever 2.0 implements ideas suggested in [1]. In general we added support for verification of software written in the GNU C programming language. First examples of using Klever for software that differs from Linux device drivers are verification of Linux kernel subsystems [2] and BusyBox applets. We are looking forward for more success stories!
Most important changes in Klever
2.0 are the following:
- Klever does not build programs under verification anymore. Instead it takes as input build bases that should be prepared with Clade in advance. This considerably speed ups verification when verifying the same software within different verification jobs. Also, this provides a more natural way to integrate Klever within a standard development life cycle.
- The generator of program fragments (former verification objects) includes abstract means suitable for various software as well as means for particular kinds of programs that allow to avoid considerable efforts for configuring program decomposition.
- The environment models generator consists of a number sub-generators that take specifications in suitable specific formats. This allows to simplify development of such the specifications very much. Besides, we fixed many existing and developed new environment model specifications both for new kinds of interactions between Linux kernel and BusyBox components and for new versions of the Linux kernel.
- The Klever interface provides users with a extremely useful online editor that enables changing configuration and specification files directly within the interface.
As usual many minor improvements and bug fixes were included in Klever 2.0.
Klever 2.0 differs too much from previous versions of Klever. Therefore, we recommend to deploy it from scratch rather than to update existing deployments.
We would like to thank everybody who participated in development, testing and using of Klever!
References
- Novikov E., Zakharov I. (2018) Towards Automated Static Verification of GNU C Programs. In: Petrenko A., Voronkov A. (eds) Perspectives of System Informatics. PSI 2017. Lecture Notes in Computer Science, vol 10742. Springer, Cham.
- Novikov E., Zakharov I. (2018) Verification of Operating System Monolithic Kernels Without Extensions. In: Margaria T., Steffen B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science, vol 11247. Springer, Cham.
Fortress:
Fortress v0.4.33 released
