|
|
Averest is a framework for the specification, verification, and implementation of reactive systems. It includes a compiler for synchronous programs, a symbolic model checker, and a tool for hardware and/or software synthesis. Averest can be used for modeling and verifying finite as well as infinite state systems at various levels of abstraction. In particular, Averest is not only well-suited for hardware design, but also for modeling communication protocols, concurrent programs, software in embedded systems, etc.
aver / /• verb (averred, averring) formal assert to be the case. — ORIGIN Old French avérer, from Latin verus ‘true’. |
Averest has been developed by the Reactive Systems Group at the University of Kaiserslautern. For more information, see the overview and the documentation. Executables and examples can be obtained on the download page. If you have any questions or comments regarding our tools or web pages, please contact us.
24 Sep 2007: Averest 1.9.3 released. In contrast to the previous versions, Averest 1.9.3 is now (almost) completely statically linked to ease installation and to improve compatibility.
24 Aug 2007: Averest 1.9.2 released. This version contains a number of improvements and some bugfixes. For more information, please see the CHANGES file contained in the distribution.
30 Nov 2006: Minor bug fixes and changes in the Eclipse plugin. See the instructions on how to update the plugin.
29 Nov 2006: Averest 1.9 released. Averest 1.9 has been released. The Eclipse plugin now supports execution of the Averest tools on our server. Additionally, the Quartz compiler employs improved translations of linear temporal logic formulas to finite automata.
30 May 2006: Averest 1.8 released. Besides several improvements and bug fixes, this release supports the new syntax of the synchronous language Quartz.