Henny Sipma: Research links

• EE380

Scientific Search

• Stanford University Libraries.
• Socrates.
• SciSearch, Los Alamos Research Library: scientific journals and citation index (Stanford only).
• MathSciNet, American Mathematical Society, mathematical reviews.
• ACM Digital Library.

Hybrid Systems

• Resources
  • HYSCOM, IEEE Control System Society Technical Committe on Hybrid Systems.
  • IEEE Working Group on Hybrid Dynamical Systems.
  • Virtual Action Group on Hybrid Dynamic Systems.
  • Santa Clara Valley IEEE CSS.
• Conferences
  • HS2000, Hybrid Systems, Computation and Control, Pittsburgh, March 23-25, 2000.
  • HS'99, Hybrid Systems, Computation and Control, Nijmegen, March 29-31, 1999.

Formal Methods

• Resources
  • Logic at Stanford.
  • Virtual Library of Formal Methods.
  • Formal methods around the world.
  • Formal methods Europe.
  • Protagonist, Proof Tools Group, Netherlands.
  • LICS Newsletter.
  • Concurrency list.
  • FME Formal Methods Applications Database.
  • Concurrency mailing list archive.
  • Roadmap to Infinite Results.
• Academia (People)
  • Rajeev Alur at the University of Pennsylvania.
  • Edmund Clarke at the CS department at CMU.
  • Rance Cleaveland, North Carolina State University.
  • Dennis Dams, at Eindhoven University of Technology.
  • Matthew Dwyer, at Kansas State University.
  • Farn Wang, at Academia Sinica, Taiwan.
  • Kathi Fisler at Rice University.
  • Orna Grumberg, at the Technion in Israel.
  • Nicholas Halbwachs at Verimag.
  • Tom Henzinger at Berkeley.
  • Nancy Lynch, at the Theory of Computation Group at MIT.
  • Jonathan Ostroff at York University, Canada.
  • Pao-Ann Hsiung, at the Academia Sinica, Taiwan.
  • Amir Pnueli, at the Weizmann Institute in Rehovot.
  • Scott Smolka, State University of New York, Stony Brook.
  • Muffy Thomas, University of Glasgow, Scotland.
  • Frits Vaandrager, at the University of Nijmegen, the Netherlands.
  • Moshe Y. Vardi, at Rice University in Houston.
  • Pierre Wolper, University of Liege, Belgium.
• Academia (Research groups)
  • BRICS. Basic Research in Computer Science. Danish National Research Foundation.
  • Hardware Verification Group at the University of Karlsrule
  • Tools for design, analysis and construction of systems, UCSB
    under supervision of P.M. Melliar-Smith and L.E. Moser.
  • VERIMAG, Grenoble, France.
  • Visual Inference Laboratory at Indiana University.
  • VIRES, Verifying Industrially Relevant Systems, Eindhoven University of Technology.
  • IMPROVE, Implementing Protocol Verification for E-commerce, University of Dublin.
• Research Institutes
  • CWI: Centrum voor Wiskunde en Informatica, Amsterdam.
  • SRI - Formal Methods.
  • Kestrel Institute.
  • IFAD,providing services and training in formal methods (Denmark).
• Industry
  • DEC - Systems Research Center
  • Computing Sciences Research Center at Bell Labs, part of Lucent Technologies.
• Electronic Journals
  • SIGACT NEWS
  • Journal of Automated Reasoning
  • Electronic Notes in Theoretical Computer Science, Elsevier.
• Journals:
  • Information and Computation.
• Miscellaneous
  • IFIP WG10.5 Benchmark Circuits for Hardware Verification.
  • SDCR: Strategic Directions in Computing Research.
  • LEDA, A platform for combinatorial and geometric computing, at the Max Planck Institute for Computer Science.
• Formal methods in Chemical Engineering
  • Joerg Preussig, University of Dortmund, Germany.

Verification Tools

The Stanford Temporal Prover

Formal Methods Tools Database.

Concurrency workbench of North Carolina

developed by Rance Cleaveland, a modelchecker for finite-state systems.

EPSILON

Verification tool for real-time systems, developed at Aalborg University, Denmark.

PAX

Tool for verification of parameterized systems.

HyTech

developed by Tom Henzinger, a modelchecker for hybrid systems.

KRONOS:

verification tool for real-time systems, developed at VERIMAG.

Murphi

developed by David Dill, a modelchecker for finite-state systems.

PARAGON:

a tool for visual specification and verification of real-time systems, (Process-Algebraic Analysic of Real-time Applications with Graphics Oriented Notation), developed by the University of Pennsylvania.

PVS

deductive verification system, developed at SRI.

RTGIL

verification tool for concurrent real-time systems, developed at UCSB.

SPIN

LTL modelchecker for distributed systems, developed at AT&T.

UPPAAL

a toolsuite for verification of real-time systems.

VIS

a system for formal verification, synthesis, and simulation of finite-state systems, developed at Berkeley.

SGM

A High-Level Specification/Verification Tool for Real-Time Concurrent Systems

VeriSoft

a tool for software developers and testers of concurrent/reactive/real-time systems, developed at AT&T

Control

• Academia
  • Karl Johan Astrom at the Department of Automatic Control at the Lund Institute of Technology.
  • Stephen Boyd, at Stanford University.
  • Shankar Sastry, at the EECS department at Berkeley.
  • Claire Tomlin, at Stanford University.
  • SHIFT, University at Berkeley.
  • Bruce Krogh at the ECE department at CMU.
  • Michael Branicki at the EECS department at MIT.
  • Murray Wonham, at the University of Toronto.
• Industry
  • AspenTech.
  • General Electric.
  • Rockwell, Palo Alto.
  • Rockwell Automation - Allen Bradley.
• Resources
  • Industrial Control and Plant Automation Home pages
  • PLCOpen: Standardization in Industrial Control Programming.
  • Control Engineering Virtual Library.
  • PLC information
  • PLC Tutor
• Miscellaneous
  • Perspectives on the future of Automation Control, a white paper.
  • OLE for Process Control Specification.
  • VISSIM, visual blockdiagram language for nonlinear dynamic simulation.

• Academia
  • University of Dortmund, Verification of hybrid controllers
• Resources
  • International Directory of Chemical Engineering URLs.

• IEEE
• ACM
• KNCV, Royal Dutch Chemical Association
• KIVI, Royal Dutch Institute of Engineers.

• NSF: National Science Foundation.
  • CCR: Computer and Computation Research.
  • CISE: NSF Directorate for Computer and Information Science Engineering.
  • Proposal guide, as per Jan 1, 2002.
• ONR: Office of Naval Research.
• NRL: Naval Research Laboratory.
• AFOSR: Air Force Science and Technology.
• DARPA: Defense Advance Research Project Agency.
• ARL: Army Research Lab.
• ARO: Army Research Office.

• Lawrence Berkeley National Lab Network Research Group