Projects
-
- Quanser 3DOF open database
Initiative to collect various level of specification for the quanser 3DOF helicopter.
For a direct access to the files: svn co https://cavale.enseeiht.fr/svn/qod
- CristalCaveGem
This project is the main repository for the development of the CristalCaveGem tool set.
- GAL Lib
Set of scripts and matlab functions to preprocess a Simulink model to enable its use through GAL (GeneAuto Lustre)
- LustreC
Lustre compiler toolset.
lustrec is structured around the modular compilation scheme proposed by Biernacki, Colaço, Hamon, and Pouzet at LCTES'08.
It is an open source lustre compiler that provides verification capabilities.
It is currently mainly used through the CocoSim platform, a Matlab toolbox to perform V&V of Simulink models. Within CocoSim, the Lustre language is used as an intermediate representation and relies mainly on lustrec to produce code or verification artifacts....
- LustreEditor
Lustre Editor
- OSDP: OCaml Semi Definite Programming
Main public page is actually https://cavale.enseeiht.fr/osdp
Registered users may use the svn repo:
svn co https://cavale.enseeiht.fr/svn/osdp - Assumptio
Actor-based Smtlib-2 Scala Unified Malleable Package for real-Time Interaction On-demand.¶
Assumptio is an actor-based SMT lib 2.0 API written in Scala designed to allow its user to perform on the fly queries to a SMT solver, which internal state is maintained until closed by the user. As of today, only Microsoft Research's Z3 and University of Trento's MathSat 5 are supported. No matter how much the authors would like to add support for other solvers, it is very difficult to do so without proper user feedback and/or contribution. This is why Assumptio is released under the GPL license. We would like to convince Assumptio's potential users that it is easy to use, and most of all relatively easy to tweak. People wanting to participate are encouraged to send their customisations to the author in order to help Assumptio improving for the best of its users....
Also available in: Atom