PI: Professor Kristin Yvonne Rozier

E-mail: kyrozier@iastate.edu

Office: 2335 Howe Hall

Laboratory: Howe 0328

Laboratory for Temporal Logic
Resources Links Page

LaTeX Resources

Other research laboratories offer relevant examples of LaTeX files. Here are a few:

Git Resources

Formal Methods Tools

Spin Model Checker

http://spinroot.com/
nuXmv Model Checker
https://es-static.fbk.eu/tools/nuxmv/
PVS Theorem Prover
http://pvs.csl.sri.com/
PRISM Model Checker
http://www.prismmodelchecker.org/
Dafny Language and Program Verifier
http://rise4fun.com/dafny/
Z3 SMT Solver
https://github.com/Z3Prover/z3
CBMC (Bounded Model Checker for C and C++ programs)
http://www.cprover.org/cbmc/


You may either install these tools on your local machine or run them on ISU's remote linux servers. The tools can be run via a remote desktop connection (e.g., ssh -Y -X) to linuxremote1.engineering.iastate.edu through linuxremote4.engineering.iastate.edu. You must be on-campus or connected to the VPN from off-campus to reach these systems. For example, 'spin' and 'ispin' run from the command line. These applications are installed in /opt/Spin. All of the examples, documentation, etc. can be found there. PVS and nuXmv are also available on the linux remote servers.

Links
Research
Blog
Publications
Home