averest
Model-based Design of Reactive Embedded Systems
About Averest
Averest is a framework for the model-based design of reactive systems that supports the modeling, specification, simulation, compilation, formal verification, and synthesis of hardware and software for reactive embedded systems. It contains compilers for synchronous languages, a simulator for the latter, support for formal verification with temporal and other logics, and various transformations for the hardware and software synthesis of reactive embedded systems which also covers pure hardware circuits and pure software systems. Averest is developed by the Embedded Systems Group at the RPTU in Kaiserslautern and is the result of a long-term and still ongoing research effort.
Overall Design Flow
There is no unique design flow using Averest but, a typical design flow consists of the following steps:
- modeling the system behavior by our synchronous language Quartz
- compilation of the Quartz model to synchronous guarded actions (the intermediate system representation of Averest)
- simulation, causality/clock analysis, and formal verification
- possible partitioning into distributed weakly endochronous components
- code synthesis as HW or SW components
- Aggregate data types like arrays and tuples can be translated to scalar data types by
Averest.Transform.Scalarize
. - Bounded range numbers and bitvectors can be reduced to booleans using
Averest.Transform.Bitblast
to finally obtain simple boolean models that can be used for model checking and for hardware circuit synthesis. - Specifications given in linear temporal logic (LTL) are translated to omega-automata and/or fixpoints in CTL and the µ-calculus where the membership to safety, liveness, and fairness classes of temporal logic are respected.
The following text explains the above steps in terms of the namespaces of the Averest library. For more details, please consult the API reference documentation.
The Synchronous Language Quartz
Synchronous languages are well-suited for the design of reactive systems. Their common paradigm is the perfect synchrony which means that most of the statements are executed as micro steps in zero time. Consumption of time is explicitly programmed by partitioning the micro steps using pause statements into macro steps that all take the same amount of logical time. Thus, concurrent threads run in lockstep and automatically synchronize at the end of a macro step. The introduction of micro and macro steps is not only a convenient programming model, it is also the key to generate deterministic single-threaded code from multi-threaded synchronous programs. Thus, synchronous programs can be executed on ordinary microcontrollers without complex process management. As another advantage, the translation of synchronous programs to circuits is straightforward since both share the same model of computation. Moreover, the formal semantics of synchronous languages makes them particularly attractive for reasoning about program semantics and correctness. Further information on Quartz can be found in the following sources (see also the example programs below):
Compilation
The compiler functions under Averest.Quartz.Compile
are used to translate Quartz programs to synchronous guarded actions which are defined in Averest.Systems.Aif
. Most parts of the translation of Quartz statements to guarded actions have been formally verified. In particular, the translation covers schizophrenic local declarations which is a nontrivial issue in the compilation of synchronous languages.
The Averest Intermediate Format (AIF) defined in Averest.Systems.Aif
is used in Averest as the intermediate representation of systems. The following transformations are mainly based on converting AIF systems and modules into special forms for the further formal verification or synthesis.
Code Transformations
Averest provides various transformations under Averest.Transform
to transform the AIF systems into equivalent ones. Most importantly, there are the following transformations:
Formal Verification
The namespace Averest.Analyze
provides functions for the analysis like formal verification. In particular, it provides its own implementation of BDDs (binary decision diagrams) and its own SAT solver as well as solvers for ILP problems based on the simplex algorithm and the Fourier-Motzkin elimination. There are also efficient functions for translating temporal logic to omega-automata, and in particular to deterministic omega-automata.
Installation, API Reference and Examples
Installation
Averest has been implemented in F# under .NET core and can therefore be used under Windows, Linux, and macOS. Averest is provided as a NuGet library and tool under the following address: https://www.nuget.org/packages/Averest which makes its use very convenient: All you need is the latest dotnet SDK which you can download from https://dotnet.microsoft.com/en-us/download for your computer.
Once you have installed dotnet, you may open an F# interactive session and just have to type #r "nuget: Averest";;
to download the latest version of Averest in your session. After this, you can open the modules to use the functions provided by Averest (see the API reference documentation). If you want to use Averest for your own software project, all you need is to add the package reference
in your project file.
Downloads
There is now also an executable command line program called AverestExe that offers many command line options that read and write files. This tool can either be installed as dotnet tool or as an executable binary file for your platform. The dotnet tool can be obtained as a nuget like the Averest library, and the executable files for some platforms are available here:
- Linux, x64 ELF binary
- Windows, x64 PE32+ executable
- Mac OSX, x64 Mach-O executable
- Mac OSX, arm64 Mach-O executable
- platform-independent nuget
API Reference
The API reference documentation lists details about the functions contained in the Averest package.
Quartz Program Examples
-
-
-
-
- TestCircuitIntAddCLAOpt
- TestCircuitIntAddCRA
- TestCircuitIntDivNonperform
- TestCircuitIntDivNonrestore
- TestCircuitIntDivRestore
- TestCircuitIntLes
- TestCircuitIntMulBooth
- TestCircuitIntMulCRACRA
- TestCircuitIntMulCRACRA_V0
- TestCircuitIntMulCRACRA_V1
- TestCircuitIntMulCSACRA
- TestCircuitIntSubCLAOpt
- TestCircuitIntSubCRA
- TestCircuitNatAddCLAOpt
- TestCircuitNatAddCRA
- TestCircuitNatDivNonperform
- TestCircuitNatDivNonrestore
- TestCircuitNatDivRestore
- TestCircuitNatLes
- TestCircuitNatMulCRACRA
- TestCircuitNatMulCSACRA
- TestCircuitNatSubCLAOpt
- TestCircuitNatSubCRA
- TestInt2Sgn
- TestIntAddCRA
- TestIntDivNonrestore
- TestIntDivRestore
- TestIntDivSeq0
- TestIntDivSeq1
- TestIntEqu
- TestIntFullAdd
- TestIntFullSub
- TestIntLes
- TestIntMulCRACRA
- TestIntMulCSACRA
- TestIntSubCRA
- TestNatAddCLA
- TestNatAddCLAOpt
- TestNatAddCRA
- TestNatDivNonrestore
- TestNatDivNonrestoreOpt
- TestNatDivNonrestoreOptCombRadix2
- TestNatDivNonrestoreOptRadix2
- TestNatDivRestore
- TestNatDivRestoreRadix2
- TestNatDivSeq0
- TestNatDivSeq1
- TestNatEqu
- TestNatFullAdd
- TestNatFullSub
- TestNatLes
- TestNatMulCRACRA
- TestNatMulCSACRA
- TestNatSubCLAOpt
- TestNatSubCRA
- TestSgn2Int
- TestSgn2IntPrinciple
- TestSgnAdd
- TestSgnCmp
- TestSgnEqu
- TestSgnLes
- TestSgnSub
-
- FixedSquareRoot
- Float2RealTable
- FloatAbs
- FloatAdd
- FloatCompareGreater
- FloatCompareGreaterEqual
- FloatCompareGreaterUnordered
- FloatCompareLess
- FloatCompareLessEqual
- FloatCompareLessUnordered
- FloatCompareNotGreater
- FloatCompareNotLess
- FloatCompareQuietEqual
- FloatCompareQuietNotEqual
- FloatCompareQuietOrdered
- FloatCompareUnordered
- FloatConstants
- FloatConvertFromInt
- FloatConvertToInteger
- FloatCopySign
- FloatDiv
- FloatIsFinite
- FloatIsInfinite
- FloatIsNaN
- FloatIsNormal
- FloatIsSignMinus
- FloatIsSubnormal
- FloatIsZero
- FloatLog
- FloatMult
- FloatNegate
- FloatSquareRoot
- IntSquareRoot
-
- FullAdd
- IntAddCLAOpt
- IntAddCRA
- IntDivNonperform
- IntDivNonrestore
- IntDivRestore
- IntLes
- IntMulBooth
- IntMulCRACRA
- IntMulCRACRA_V0
- IntMulCRACRA_V1
- IntMulCSACRA
- IntSubCLAOpt
- IntSubCRA
- LesCell
- NatAddCLAOpt
- NatAddCRA
- NatDivNonperform
- NatDivNonrestore
- NatDivRestore
- NatLes
- NatMulCRACRA
- NatMulCSACRA
- NatSubCLAOpt
- NatSubCRA
- SgnAdd
- SgnEqu
- SgnFullAdd
- SgnLes
- SgnSub
-
- Horner
- IntAddCRA
- IntDivAlgo
- IntDivNonrestore
- IntDivRestore
- IntDivSeq0
- IntDivSeq1
- IntEqu
- IntFullAdd
- IntFullSub
- IntLes
- IntMulCRACRA
- IntMulCSACRA
- IntSubCRA
- NatAddCLA
- NatAddCLAOpt
- NatAddCRA
- NatDivAlgo
- NatDivNonrestore
- NatDivNonrestoreOpt
- NatDivNonrestoreOptCombRadix2
- NatDivNonrestoreOptRadix2
- NatDivRestore
- NatDivRestoreRadix2
- NatDivSeq0
- NatDivSeq1
- NatEqu
- NatFullAdd
- NatFullSub
- NatLes
- NatMulCRACRA
- NatMulCSACRA
- NatSubByCompl
- NatSubCLA
- NatSubCLAOpt
- NatSubCRA
- ToBComplement
- ToRadixB
-
-
- DecompCholesky
- DecompLU
- DecompLU2
- DecompLUP
- DecompQR
- DecompQRC
- EigenvaluesQR
- EigenvaluesShift2QR
- EigenvaluesShiftQR
- EigenvaluesShiftQRC
- GramSchmidt
- InverseGaussJordan
- LinearEquGaussJordan
- LinearEquGaussJordanRat
- LinearEquLU
- LinearEquLUP
- MatrixMultCannon
- MatrixMultCombLogN
- MatrixMultCombN
- MatrixMultSeq
-
-
-
-
-
- FullAdd
- IntAddCLAOpt
- IntAddCRA
- IntDivNonperform
- IntDivNonrestore
- IntDivRestore
- IntLes
- IntMulBooth
- IntMulCRACRA
- IntMulCRACRA_V0
- IntMulCRACRA_V1
- IntMulCSACRA
- IntSubCLAOpt
- IntSubCRA
- LesCell
- NatAddCLAOpt
- NatAddCRA
- NatDivNonperform
- NatDivNonrestore
- NatDivRestore
- NatLes
- NatMulCRACRA
- NatMulCSACRA
- NatSubCLAOpt
- NatSubCRA
- SgnAdd
- SgnEqu
- SgnFullAdd
- SgnLes
- SgnSub
-
-
-
-
MiniC Program Examples
-
-
-
- BinaryTree_Arr_1024
- BinaryTree_Arr_128
- BinaryTree_Arr_16
- BinaryTree_Arr_256
- BinaryTree_Arr_32
- BinaryTree_Arr_4
- BinaryTree_Arr_512
- BinaryTree_Arr_64
- BinaryTree_Arr_8
- BinaryTree_Scl_1024
- BinaryTree_Scl_128
- BinaryTree_Scl_16
- BinaryTree_Scl_256
- BinaryTree_Scl_32
- BinaryTree_Scl_4
- BinaryTree_Scl_512
- BinaryTree_Scl_64
- BinaryTree_Scl_8
- BitonicSort_16
- BitonicSort_32
- BitonicSort_4
- BitonicSort_64
- BitonicSort_8
- EvalPolynomial_ArrGlb_128
- EvalPolynomial_ArrGlb_16
- EvalPolynomial_ArrGlb_256
- EvalPolynomial_ArrGlb_32
- EvalPolynomial_ArrGlb_4
- EvalPolynomial_ArrGlb_512
- EvalPolynomial_ArrGlb_64
- EvalPolynomial_ArrGlb_8
- EvalPolynomial_ArrLoc_128
- EvalPolynomial_ArrLoc_16
- EvalPolynomial_ArrLoc_256
- EvalPolynomial_ArrLoc_32
- EvalPolynomial_ArrLoc_4
- EvalPolynomial_ArrLoc_512
- EvalPolynomial_ArrLoc_64
- EvalPolynomial_ArrLoc_8
- EvalPolynomial_SclGlb_128
- EvalPolynomial_SclGlb_16
- EvalPolynomial_SclGlb_256
- EvalPolynomial_SclGlb_32
- EvalPolynomial_SclGlb_4
- EvalPolynomial_SclGlb_512
- EvalPolynomial_SclGlb_64
- EvalPolynomial_SclGlb_8
- EvalPolynomial_SclLoc_128
- EvalPolynomial_SclLoc_16
- EvalPolynomial_SclLoc_256
- EvalPolynomial_SclLoc_32
- EvalPolynomial_SclLoc_4
- EvalPolynomial_SclLoc_512
- EvalPolynomial_SclLoc_64
- EvalPolynomial_SclLoc_8
- FastFourierTransform_ArrGlb_128
- FastFourierTransform_ArrGlb_16
- FastFourierTransform_ArrGlb_256
- FastFourierTransform_ArrGlb_32
- FastFourierTransform_ArrGlb_4
- FastFourierTransform_ArrGlb_64
- FastFourierTransform_ArrGlb_8
- FastFourierTransform_ArrLoc_128
- FastFourierTransform_ArrLoc_16
- FastFourierTransform_ArrLoc_256
- FastFourierTransform_ArrLoc_32
- FastFourierTransform_ArrLoc_4
- FastFourierTransform_ArrLoc_64
- FastFourierTransform_ArrLoc_8
- FastFourierTransform_SclGlb_128
- FastFourierTransform_SclGlb_16
- FastFourierTransform_SclGlb_256
- FastFourierTransform_SclGlb_32
- FastFourierTransform_SclGlb_4
- FastFourierTransform_SclGlb_64
- FastFourierTransform_SclGlb_8
- FastFourierTransform_SclLoc_128
- FastFourierTransform_SclLoc_16
- FastFourierTransform_SclLoc_256
- FastFourierTransform_SclLoc_32
- FastFourierTransform_SclLoc_4
- FastFourierTransform_SclLoc_64
- FastFourierTransform_SclLoc_8
- MatrixMultCannon_ArrGlb_10
- MatrixMultCannon_ArrGlb_2
- MatrixMultCannon_ArrGlb_3
- MatrixMultCannon_ArrGlb_4
- MatrixMultCannon_ArrGlb_5
- MatrixMultCannon_ArrGlb_6
- MatrixMultCannon_ArrGlb_7
- MatrixMultCannon_ArrGlb_8
- MatrixMultCannon_ArrGlb_9
- MatrixMultCannon_ArrLoc_10
- MatrixMultCannon_ArrLoc_2
- MatrixMultCannon_ArrLoc_3
- MatrixMultCannon_ArrLoc_4
- MatrixMultCannon_ArrLoc_5
- MatrixMultCannon_ArrLoc_6
- MatrixMultCannon_ArrLoc_7
- MatrixMultCannon_ArrLoc_8
- MatrixMultCannon_ArrLoc_9
- MatrixMultCannon_SclGlb_10
- MatrixMultCannon_SclGlb_2
- MatrixMultCannon_SclGlb_3
- MatrixMultCannon_SclGlb_4
- MatrixMultCannon_SclGlb_5
- MatrixMultCannon_SclGlb_6
- MatrixMultCannon_SclGlb_7
- MatrixMultCannon_SclGlb_8
- MatrixMultCannon_SclGlb_9
- MatrixMultCannon_SclLoc_10
- MatrixMultCannon_SclLoc_2
- MatrixMultCannon_SclLoc_3
- MatrixMultCannon_SclLoc_4
- MatrixMultCannon_SclLoc_5
- MatrixMultCannon_SclLoc_6
- MatrixMultCannon_SclLoc_7
- MatrixMultCannon_SclLoc_8
- MatrixMultCannon_SclLoc_9
- MatrixMultSimple_ArrGlb_10
- MatrixMultSimple_ArrGlb_2
- MatrixMultSimple_ArrGlb_3
- MatrixMultSimple_ArrGlb_4
- MatrixMultSimple_ArrGlb_5
- MatrixMultSimple_ArrGlb_6
- MatrixMultSimple_ArrGlb_7
- MatrixMultSimple_ArrGlb_8
- MatrixMultSimple_ArrGlb_9
- MatrixMultSimple_ArrLoc_10
- MatrixMultSimple_ArrLoc_2
- MatrixMultSimple_ArrLoc_3
- MatrixMultSimple_ArrLoc_4
- MatrixMultSimple_ArrLoc_5
- MatrixMultSimple_ArrLoc_6
- MatrixMultSimple_ArrLoc_7
- MatrixMultSimple_ArrLoc_8
- MatrixMultSimple_ArrLoc_9
- MatrixMultSimple_SclGlb_10
- MatrixMultSimple_SclGlb_2
- MatrixMultSimple_SclGlb_3
- MatrixMultSimple_SclGlb_4
- MatrixMultSimple_SclGlb_5
- MatrixMultSimple_SclGlb_6
- MatrixMultSimple_SclGlb_7
- MatrixMultSimple_SclGlb_8
- MatrixMultSimple_SclGlb_9
- MatrixMultSimple_SclLoc_10
- MatrixMultSimple_SclLoc_2
- MatrixMultSimple_SclLoc_3
- MatrixMultSimple_SclLoc_4
- MatrixMultSimple_SclLoc_5
- MatrixMultSimple_SclLoc_6
- MatrixMultSimple_SclLoc_7
- MatrixMultSimple_SclLoc_8
- MatrixMultSimple_SclLoc_9
- MatrixMultStrassenWinograd_ArrGlb_4
- MatrixMultStrassenWinograd_ArrGlb_8
- MatrixMultStrassenWinograd_ArrLoc_4
- MatrixMultStrassenWinograd_ArrLoc_8
- MatrixMultStrassenWinograd_SclGlb_4
- MatrixMultStrassenWinograd_SclGlb_8
- MatrixMultStrassenWinograd_SclLoc_4
- MatrixMultStrassenWinograd_SclLoc_8
- ParallelPrefixTree_ArrGlb_128
- ParallelPrefixTree_ArrGlb_16
- ParallelPrefixTree_ArrGlb_256
- ParallelPrefixTree_ArrGlb_32
- ParallelPrefixTree_ArrGlb_4
- ParallelPrefixTree_ArrGlb_512
- ParallelPrefixTree_ArrGlb_64
- ParallelPrefixTree_ArrGlb_8
- ParallelPrefixTree_ArrLoc_128
- ParallelPrefixTree_ArrLoc_16
- ParallelPrefixTree_ArrLoc_256
- ParallelPrefixTree_ArrLoc_32
- ParallelPrefixTree_ArrLoc_4
- ParallelPrefixTree_ArrLoc_512
- ParallelPrefixTree_ArrLoc_64
- ParallelPrefixTree_ArrLoc_8
- ParallelPrefixTree_SclGlb_128
- ParallelPrefixTree_SclGlb_16
- ParallelPrefixTree_SclGlb_256
- ParallelPrefixTree_SclGlb_32
- ParallelPrefixTree_SclGlb_4
- ParallelPrefixTree_SclGlb_512
- ParallelPrefixTree_SclGlb_64
- ParallelPrefixTree_SclGlb_8
- ParallelPrefixTree_SclLoc_128
- ParallelPrefixTree_SclLoc_16
- ParallelPrefixTree_SclLoc_256
- ParallelPrefixTree_SclLoc_32
- ParallelPrefixTree_SclLoc_4
- ParallelPrefixTree_SclLoc_512
- ParallelPrefixTree_SclLoc_64
- ParallelPrefixTree_SclLoc_8
- RadixBAddCarryLookahead_ArrGlb_128
- RadixBAddCarryLookahead_ArrGlb_16
- RadixBAddCarryLookahead_ArrGlb_256
- RadixBAddCarryLookahead_ArrGlb_32
- RadixBAddCarryLookahead_ArrGlb_4
- RadixBAddCarryLookahead_ArrGlb_64
- RadixBAddCarryLookahead_ArrGlb_8
- RadixBAddCarryLookahead_ArrLoc_128
- RadixBAddCarryLookahead_ArrLoc_16
- RadixBAddCarryLookahead_ArrLoc_256
- RadixBAddCarryLookahead_ArrLoc_32
- RadixBAddCarryLookahead_ArrLoc_4
- RadixBAddCarryLookahead_ArrLoc_64
- RadixBAddCarryLookahead_ArrLoc_8
- RadixBAddCarryLookahead_SclGlb_128
- RadixBAddCarryLookahead_SclGlb_16
- RadixBAddCarryLookahead_SclGlb_256
- RadixBAddCarryLookahead_SclGlb_32
- RadixBAddCarryLookahead_SclGlb_4
- RadixBAddCarryLookahead_SclGlb_64
- RadixBAddCarryLookahead_SclGlb_8
- RadixBAddCarryLookahead_SclLoc_128
- RadixBAddCarryLookahead_SclLoc_16
- RadixBAddCarryLookahead_SclLoc_256
- RadixBAddCarryLookahead_SclLoc_32
- RadixBAddCarryLookahead_SclLoc_4
- RadixBAddCarryLookahead_SclLoc_64
- RadixBAddCarryLookahead_SclLoc_8
- RadixBMulDadda_ArrGlb_10
- RadixBMulDadda_ArrGlb_11
- RadixBMulDadda_ArrGlb_12
- RadixBMulDadda_ArrGlb_13
- RadixBMulDadda_ArrGlb_14
- RadixBMulDadda_ArrGlb_15
- RadixBMulDadda_ArrGlb_16
- RadixBMulDadda_ArrGlb_17
- RadixBMulDadda_ArrGlb_18
- RadixBMulDadda_ArrGlb_19
- RadixBMulDadda_ArrGlb_4
- RadixBMulDadda_ArrGlb_5
- RadixBMulDadda_ArrGlb_6
- RadixBMulDadda_ArrGlb_7
- RadixBMulDadda_ArrGlb_8
- RadixBMulDadda_ArrGlb_9
- RadixBMulDadda_ArrLoc_10
- RadixBMulDadda_ArrLoc_11
- RadixBMulDadda_ArrLoc_12
- RadixBMulDadda_ArrLoc_13
- RadixBMulDadda_ArrLoc_14
- RadixBMulDadda_ArrLoc_15
- RadixBMulDadda_ArrLoc_16
- RadixBMulDadda_ArrLoc_17
- RadixBMulDadda_ArrLoc_18
- RadixBMulDadda_ArrLoc_19
- RadixBMulDadda_ArrLoc_4
- RadixBMulDadda_ArrLoc_5
- RadixBMulDadda_ArrLoc_6
- RadixBMulDadda_ArrLoc_7
- RadixBMulDadda_ArrLoc_8
- RadixBMulDadda_ArrLoc_9
- RadixBMulDadda_SclGlb_10
- RadixBMulDadda_SclGlb_11
- RadixBMulDadda_SclGlb_12
- RadixBMulDadda_SclGlb_13
- RadixBMulDadda_SclGlb_14
- RadixBMulDadda_SclGlb_15
- RadixBMulDadda_SclGlb_16
- RadixBMulDadda_SclGlb_17
- RadixBMulDadda_SclGlb_18
- RadixBMulDadda_SclGlb_19
- RadixBMulDadda_SclGlb_4
- RadixBMulDadda_SclGlb_5
- RadixBMulDadda_SclGlb_6
- RadixBMulDadda_SclGlb_7
- RadixBMulDadda_SclGlb_8
- RadixBMulDadda_SclGlb_9
- RadixBMulDadda_SclLoc_10
- RadixBMulDadda_SclLoc_11
- RadixBMulDadda_SclLoc_12
- RadixBMulDadda_SclLoc_13
- RadixBMulDadda_SclLoc_14
- RadixBMulDadda_SclLoc_15
- RadixBMulDadda_SclLoc_16
- RadixBMulDadda_SclLoc_17
- RadixBMulDadda_SclLoc_18
- RadixBMulDadda_SclLoc_19
- RadixBMulDadda_SclLoc_4
- RadixBMulDadda_SclLoc_5
- RadixBMulDadda_SclLoc_6
- RadixBMulDadda_SclLoc_7
- RadixBMulDadda_SclLoc_8
- RadixBMulDadda_SclLoc_9
- TransHull_ArrGlb_2
- TransHull_ArrGlb_3
- TransHull_ArrGlb_4
- TransHull_ArrGlb_5
- TransHull_ArrGlb_6
- TransHull_ArrGlb_7
- TransHull_ArrGlb_8
- TransHull_ArrLoc_2
- TransHull_ArrLoc_3
- TransHull_ArrLoc_4
- TransHull_ArrLoc_5
- TransHull_ArrLoc_6
- TransHull_ArrLoc_7
- TransHull_ArrLoc_8
- TransHull_SclGlb_2
- TransHull_SclGlb_3
- TransHull_SclGlb_4
- TransHull_SclGlb_5
- TransHull_SclGlb_6
- TransHull_SclGlb_7
- TransHull_SclGlb_8
- TransHull_SclLoc_2
- TransHull_SclLoc_3
- TransHull_SclLoc_4
- TransHull_SclLoc_5
- TransHull_SclLoc_6
- TransHull_SclLoc_7
- TransHull_SclLoc_8
-
Research Papers
To learn more about the foundations and algorithms behind the Averest tools, see the following pages:
- publications of es.cs.uni-kl.de
- research pages of es.cs.uni-kl.de
Contact
Averest is the result of still ongoing research efforts of the chair on embedded systems at the department of computer science of the university of Kaiserslautern. As a contact person, you may contact any person of the group, in particular, the head which is:
- Prof.Dr. Klaus Schneider
- Embedded Systems Chair
- Department of Computer Science
- RPTU Kaiserslautern
- P.O. Box 3049
- 67653 Kaiserslautern, Germany
- web page