Research links

          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
            • IEEE Working Group on Hybrid Dynamical Systems.
            • Virtual Action Group on Hybrid Dynamic Systems.
          • 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 (General)

          • 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.
          • Conferences (1999)
            • AMAST'98,Amazonia, Brazil, Jan 5-9.
            • DCCA-7, Dependable Computing for Critical Applications, San Jose, Jan 6-8.
            • POPL'99, San Antonio, Jan 20-22.
            • STACS'99, Trier, Germany, March 4-6.
            • FemSys'99, Munich, March 15-17.
            • FOSSACS'99, Foundations of Software Science and Computation Structures, Amsterdam, March 22-26.
            • TACAS'99, Amsterdam, March 22-26.
            • HS'99, Hybrid Systems, Computation and Control, Nijmegen, March 29-31.
            • ARTS'99, Bamberg, Germany, May 26-28. Subm.deadline: Oct. 30.
            • LICS'99, Trento, Italy, July 2-5. Subm.deadline: Dec. 10.
            • CAV'99, Trento, Italy, July 7-10. Subm.deadline: Jan 3.
            • FM'99, Toulouse, Sept 20-24. Subm.deadline: Feb 14, 99.
          • 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.
          • 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.
          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

          Commercial verification tools

          DESIGN VERIFYer
          Hardware verification tool from Chrysalis.

          Courses in program verification

          US and Canada

          • University of Pennsylvania: Computer-Aided Verification, taught by Rajeev Alur.
          • University of Texas at Austin: Verification of Digital Systems --- Fall 1997, taught by Adnan Aziz.
          • Kansas State University: Specification and Verification of Reactive Systems, taught by Matthew Dwyer.
          • Rice University: Applied Computer-Aided Verification, taught by Kathi Fisler.
          • Stanford University: Formal methods for concurrent and reactive systems, taught by Henny Sipma.
          • York University (Canada): Introduction to Program Verification, taught by Jonathan Ostroff.

          Europe

          • Cambridge University: Specification and Verification I, taught by Mike Gordon.
          • Universitat of Bielefeld (Germany): Specification and Verification of Concurrent Systems, taught by Peter Ladkin

          Control

          • Conferences 1998
            • CDC98, Tampa, FL, Dec 16-18. Subm.deadline: March 2.
          • Conferences 1999
            • ISIC'99, Cambridge, MA, Sept 15-17. Subm.deadline: Feb 16.
          • 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.
            • 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.

          Chemical Engineering

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

          Professional Organizations

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

          Newsgroups::

          • csd: csd.bboard, phdcs, csd.colloq
          • su: su.org.i-center, su.jobs
          • comp: specification.misc, theory, risks, realtime, lang.ml, org.acm, org.ieee
          • sci: sci.logic, sci.engr.safety, sci.engr.control

          Publishers

          • Addison Wesley, Computer Science and Engineering.
          • Springer Verlag, Heidelberg.
          • Kluwer. Formal Methods in System Design is here.

          Educational resources

          • Logic
            • Teaching logic as a tool, by David Gries and Fred Schneider.

          Funding agencies

          • NSF: National Science Foundation.
            • CCR: Computer and Computation Research.
            • CISE: NSF Directorate for Computer and Information Science Engineering.
          • 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.

          Miscellaneous resources

          • Alta Vista
          • Job search
          • xv documentation
          • room reservation
          • Java 2 Platform. Standard Edition

          © Xuandong Li / lxd@nju.edu.cn