History log of /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/Holmakefile
Revision Date Author Comments
# 32537a56 11-Oct-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Get temporal_deep/src/model_check to build by fixing Holmakefile
# 0c1bf97e 10-Oct-2018 Chun Tian (binghe) <binghe.lisp@gmail.com>

Added self tests
# 20008a7e 10-Oct-2018 Chun Tian (binghe) <binghe.lisp@gmail.com>

Fixed modelCheckLib with NuSMV model checker
# ab4a4cbb 03-Feb-2015 Piotr Trojanek <piotr.trojanek@gmail.com>

remove executable bit from text files in examples/
# 1e90d3ff 18-Oct-2006 Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk>

Some deep embeddings of temporal logics and some related tools. Especially there are translations between PSL and LTL and between LTL and omega-automata. Additionally, there is an interface to SMV