|
|
Averest is a set of tools 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/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. For more information, please refer to the Averest home page.
The HOL system is an automated proof system for higher order logic built on top of Moscow ML. It provides an environment with an expressive notation for writing system specifications and powerful facilities for creating formal proofs of properties of specifications. It has been used in many areas, including the definition of HDL semantics (e.g. VHDL, Verilog), hardware design and verification, reasoning about security, reasoning about real-time systems and software verification.
One of its most important properties is its rigorous and well-understood theoretical basis that allows users to extend the system without compromising security. The HOL system comes with an extensive library containing hundreds of predefined types, functions, tactics and proven theorems. On our HOL modules page, you find various theories and tools, which originate from our research projects and extend the standard library.
If you like Kate, the editor of the KDE desktop environment, you will certainly find kate-emmbeddedhol useful. It integrates the theorem prover into this editor.
|