Project Links
Note: These are just my hot project links that I consider interesting. If you want to know what I am doing, the Professional Info is the right place.
Links by Research Area
Decision Procedures
- Hardware Verification Group at Stanford
- Cooperating Validity Checker
- SMT-LIB: The Satisfiability Modulo Theories Library
Model Checking
- Model Checking Project page at CMU
- SyMP: a tool for combining model checking and theorem proving that I developed as a part of my Ph.D. thesis.
- SMV trial online
- CV: VHDL model checker
- Formal Methods Page (maintained by Jeannette Wing)
Theorem Proving
- PVS Theorem Proving System
- STeP - The Stanford Temporal Prover.
- The HOL System at University of Cambrigde Comuter Laboratory, UK. Another HOL page is at Brigham Young University.
- Isabelle Theorem Proving System.
- Coq
(Non)Stantard ML
My Software Projects
This section used to be called "free software," but I discovered that not all of it is exactly free, as defined by the FSF. Anyhow, here you'll find the software projects I was and am involved in.- CVC Lite: a cleaner and better re-implementation of CVC, developed at Stanford and NYU.
- Cooperating Validity Checker developed at Stanford by Clark Barrett and Aaron Stump. It is a decision procedure for a combination of quantifier-free first-order theories including linear arithmetic, arrays, datatypes, etc.
- SyMP: a tool for combining model checking and theorem proving that I developed as a part of my Ph.D. thesis.
- SMV (Symbolic Model Verifier): originally written by Ken McMillan, and I mercilessly hacked it in the late 1990's.
- Turing Machine simulator
- Light-weight backup scripts in Perl
- Javascript-based tools
- Trainer for peripheral vision
- Scrolling text to pace your reading speed
- ERC - Emacs IRC Client (GPL'ed); originally written by Alexander L. Belikoff, then I improved it in many ways and promoted to version 2.0, and eventually it was picked up by other folks who are making it part of Emacs.
- A simple SML Code demonstrating that the SML typechecker has an exponential complexity.
- My Touch-typing course on QWERTY keyboard.
Links by Research Topic
Space Shuttle Stuff
Cute Stuff
People and Places
SRI International
People of interest
- Ken McMillan's homepage at UCB
- Hardware Varification Group at Stanford (hey, I'm there now too!)
- Leslie Lamport
- Igor Walukiewicz
- Armin Biere