Sergey Berezin's Project Links (original) (raw)

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

• SML/NJ
• Objective CAML

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

• Johnson Space Center, NASA
• Space Shuttle program.
• NASA bibliography
• Space Calendar

Cute Stuff

• Aspect-Oriented Programming at Xerox PARC.

People and Places

SRI International

• Computer Science Laboratory
• People at CSL
  • Judith Crow
  • Natarajan Shankar

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