Tabular Expression Toolbox
23 Sep 2010
13 Aug 2014)
A tool for creating tabular expressions in Matlab/Simulink integrating checking with PVS and CVC3.
- Tested with Matlab Simulink 2011b, 2011a, 2010a, 2009b
- The tool supports checking of table completness and disjointness through the support of external tools
- This tool will work with either or both of the tools installed.
- It is recommened that both tools be installed, as they are built on different technologies, and have different strengths and weaknesses.
- CVC3 is supported for checking for completness and disjointness of tables
- CVC3 can be downloaded from http://cs.nyu.edu/acsys/cvc3/
- Ensure that cvc3 is executable on the shell path.
- CVC3 is available for Linux/OS X and Windows.
PVS (Prototype Verification System)
- PVS is supported for checking for completness and disjointness of tables.
- PVS is downloadable from http://pvs.csl.sri.com/
- System has been tested on PVS versions 5.0, 4.2 and 4.1
- Ensure that pvs executable is on shell path
- Note: PVS is a Linux and MacOS X application and will not run natively on Windows.