Averest
home
overview
documentation
screenshots
download
links
contact

Welcome!

Averest is a set of tools for the specification, verification, and implementation of reactive systems. It includes a compiler and a simulator for synchronous programs, a symbolic model checker and a tool for hardware-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 is currently developed by the Embedded 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.

Averest News

09 Dec 2008: Averest 2 coming soon. The upcoming version 2 of Averest will be released in January 2009. We are currently preparing the release.