WWW Virtual Library by Jonathan Bowen Repositories Who's Who Companies Z and HTML comp.specification.larch comp.specification.misc comp.specification.z
Theory and Formal Methods at Imperial College Laboratory for Applied Logic at Brigham Young University Formal Methods Elsewhere at ukc
Hardware (academic) adapted from a compilation by Sofiene Tahar Specification and Verification II - Mike Gordon, Cambridge University. Describing hardware with programs (HDLs). Using Floyd-Hoare logic and temporal logic to reason about continuously running programs and hardware. Translating programs to machines (synthesis from Verilog). Specifying structure and behaviour. Parameterised designs. Logical models of transistors. Sequential behaviour and temporal abstraction. Use of Temporal logic directly on hardware models. Linear versus branching time. Model checking for CTL. Verification of Digital Systems - A course by Adnan Aziz, University of Texas Vorlesung Hardware-Verifikation - postscript course materials (in German) by Thomas Kropf, University of Karlsruhe. new_theory `HOL`; - by Graham Birtwistle et. al. An online hypertext book providing an introduction to hardware verification in Higher Order Logic. VIS - Verification interacting with Synthesis, at UC Berkeley. Formal Specification and Verification of Hardware - Course description by Shui-Kai Chin, Syracuse University Mixed Hardware-Software Verification of Mixed Hardware-Software Systems - Alan Hu, University of British Columbia Co-Design Automation - SuperlogTM - "the future of system simulation and verification" SLDL - System Level Design Language for co-design.	Software Specification and Verification I - Mike Gordon, Cambridge University. Program specification: partial and total correctness. Hoare notation. Axioms and rules of Floyd-Hoare logic. Discussion of soundness and completeness. Mechanised program verification: verification conditions. Program refinement. Weakest preconditions. Semantic embedding in higher order logic. The Limitations of Program Verification Verisoft - a tool from Lucent Technologies for systematically exploring the state spaces of software systems composed of several concurrent processes executing arbitrary code written in full-fledged programming languages, such as C or C++. Hardware (commercial) Chrysalis - commercial EDA tools based on verification technology, white papers, and symbolic logic tutorial material. Higher Level Design Automation - from the ICL design automation group, SUPERvise, methods and tools for system level design with VHDL+, a superset of VHDL with formal system interface specifications. Abstract Design Automation - a leading provider of advanced formal verification based system design tools based on Analysis Driven Design. Lambda, Check-off and PolyML. VFormal - Finite state hardware verification from Compass Technology? Advanced Bytes and Rights Limited - hardware verification technologies based on translating higher order logic to first order logic.

Representation of Formal Notations

Z and HTML - Jonathan Bowen's page on the HTML for the formal specification language Z.

Object-Z LaTeX Macros - at the software verification research center, University of Queensland.

Math HTML -

Math HTML overview -

Action Semantics - a story on how to do formal semantics for programming languages.

proof.sty - a LaTeX2e style file by Makoto Tatsuta for formatting proof trees.

specifying web architecture with Larch - formal modelling relating to XML standards activities by Dan Connolly.

zeditor - a freeware Z editor for Windows (rtf files)..

© created 1995-10-26 modified 2004-12-23