Mr. Shenwei Yu

Research Interests

• Verification
• Smart Cards
• Java
• Security
• E-Commerce

Publications

• Implementing a Model Checker for LEGO (FME'97)
• Verification of Concurrent Programs Based on Type Theory, PhD Thesis

Useful pointers:

• Archives
• Institutions
• People
• Systems
• Links to related pages
• UK libraries

Archives:

• Imperial TCS Archive
• Tulane TCS Archive

Institutions:

• UK:
  • Universities
  • Cambridge DCS
  • Edinburgh DCS
  • Glasgow DCS
  • Imperial DCS (Theory & FM )
  • Kent DCS
  • Manchester DCS
  • Sussex DCS
  • Proof-Tools Group Netherlands
  • Working Group TYPES
• Europe:
  • Aarhus DCS
  • BRICS
  • CWI
  • Chalmers DCS
• USA and Australia:
  • CMU DCS
  • Digital SRC
  • Verification Centre at Queensland
• Japan:
  • Universities
  • Institutions including ETL
• China:
  • Universities
  • Laboratories
• Other institutions:
  • EPSRC

People:

• Imperial College Collections
• Who's Who in formal methods
• SIGACT virtual rolodex of theoretical computer scientists
• Researchers in programming languages
• Researchers in logical frameworks
• V. Pratt's list of email addresses

Systems:

• Theorem provers, including:
  • 3TAP-- a tableaux based theorem prover for many-valued first-order logics. Brief Description
  • Boyer-Moore(NQTHM)-- a prover for quantifier free logic for recursive functions over the integers and other finitely generated structures, combining rewriting, heuristics for induction, and other techniques.Brief Description
  • Coq-- a proof assistant base on the calculus of inductive constructions. Brief Description
  • HOL-- an interactive environment for machine-assisted theorem-proving in higher-order logic.Brief Description
    • HOL page at BYU (on-line documentation)
    • HOL page at Oxford
  • Isabelle-- a generic theorem prover in which logics can be specified and used.
  • Lego-- a Proof Assistant based on type theory.
  • Mizar-- a system for writing and checking formal mathematics, based on Tarski-Grothendieck set theory, and natural deduction.
  • Nuprl-- a proof system for an intuitionistic type theory based on Martin Lof type theory, with proof by refinement and extraction of programs from proofs. Brief Description
  • TPS-- a theorem proving system for first- and higher-order logic with both automatic and interactive modes. Brief Description
• Logical frameworks, including:
  • Elf-- a system based on predicative type theory that can be used to specify and reason about logics, languages, type systems, etc. Brief Description
  • Lambda Prolog
• Specification languages and verification tools, including:
  • Extended ML
  • LOTOS
  • PVS(Prototype Verification System)-- a specification/verification system based on higher-order logic. Brief Description
• Concurrent systems, including:
  • Edinburgh Concurrency Workbench (CWB) is an automated tool for manipulation and analysis of concurrent systems.
  • SMV (of CMU)
  • Spin-- an automated verification tool (model checker), based on CSP.
  • TLA (Temporal Logic of Actions), Tools
  • UNITY verify system(UV)-- an interactive symbolic model checker for UNITY.

Links to related pages:

• Technical and other mailing lists: AMAST links, Categories, Types, UK CS research, V&V links.
• Conferences in computer science: including areas such as AI, formal methods (meetings and conferences), logic (lics-maintained list), programming languages, reasoning, software engineering, and theoretical computer science.
• Computer Science Journals and Technical Reports.

UK libraries:

• UK Univ Research Libraries
• Durham (online)
• Edinburgh (online)
• York (online)