User Manual and Technical Documentation:
- The Synchronous Programming Language Quartz, Version 2.0, 2008.
PDF
- Averest Interchange Format, Version 1.2, 2006.
PDF
Publications on Averest:
- K. Schneider and T. Schuele, "A framework for verifying and implementing embedded systems". In B. Straube and M. Freibothe, editors, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pages 242-247, Dresden, Germany, 2006. PDF
- K. Schneider and T. Schuele, "Averest: Specification, verification, and implementation of reactive systems". In Conference on Application of Concurrency to System Design (ACSD), St. Malo, France, 2005. PDF
- ABRO1.qrz Generic version of the ABRO example.
- BinarySearch.qrz Find an element in a sorted array of numbers.
- BoothMult01.qrz Booth's algorithm for multiplication of integers.
- BubbleSort.qrz Sorting algorithm that has quadratic time complexity.
- Euclid.qrz Euclid's algorithm for computing the greatest common divisor of two natural numbers.
- FastMax.qrz Find the maximal element in an array of numbers in constant time using several processes.
- LTL.qrz Theorems of linear time temporal logic.
- ParallelPrefixSum.qrz Compute the sums of all prefixes of an array of integers.
- Partition.qrz Partition the elements of an array.
- Queens.qrz Place n queens on a chessboard so that no queen can attack another one.
- SquareRoot.qrz Compute the square root of a natural number.
- VendingMachine.qrz Controller for a vending machine that dispenses chewing gums.
Further examples are contained in the distribution. To learn more about the foundations and algorithms behind the Averest tools, see the publications of the Reactive Systems Group.
