H N Y 9 7 3 4 8 :

598 Graham Birtwistle

uk
uk
Credentials
B.Sc. Class I Honours (1960) Sheffield University
Ph.D. (1965) Sheffield University
D.Sc. (1988) Sheffield University
Present Position
Professor, Department of Computer Science
Key Words
Formal methods; hardware verification; concurrency theory
Formal hardware verification using the HOL (higher order logic) theorem prover. Our best effort was to specify, verify, fabricate and testthe SECD machine. This chip is at a very high level of abstraction(having built-in support for recursive function calls) and required novelwork on abstraction functions between design levels. However it is a relatively easy machine to program and at which to targetcompilers. This work was supported by an NSERC Strategic Grant (1986--89).
The re-implemention HOL in SML. The new system is faster than theold standard and more systematically engineered. It is now freelyavailable on ftp and is now in use by AT&T, Sun, Cambridge, Edinburgh,Munich, ... This work was supported by an NSERC Strategic Grant (1988--91).

Use of CCS to specify asynchronous hardware designs and its CWBsupport tool to show equivalence and prove consequences of specificationsusing process logics. We are working with the Manchester UniversityAMULET team formalising and analysing the design of their asynchronousACORN RISC machine, and on the implementation of a silicon compiler for asynchronous design.

Simulation language design and the use of simulation in designing network software (e.g. X25). The semantics of simulation languagesand applying the techniques of process algebra to simulation models (testing models for deadlock, livelock, safety and liveness properties).

Formal verification of compilers and silicon compilers: formallanguage definition and proofs of correctness of all the transformation algorithms in compilation schemata.

Languages:

References:

  • ()  E A

    Internal error

    DEFRSTCAP: [Microsoft][ODBC SQL Server Driver][SQL Server]Incorrect syntax near ')'. -2147217900 0 Microsoft OLE DB Provider for ODBC Drivers at  surtitle 
     SQL is  SELECT tblSourceDocument.lngFKPerson, tblSourceDocument.lngFKPerson AS jjjj, tblDocuments.txtFileName AS docfile, tblSourceDocument.lngFKSource, tblDocuments.* FROM tblDocuments INNER JOIN tblSourceDocument ON tblDocuments.idDocument = tblSourceDocument.lngFKDocument WHERE (((tblSourceDocument.lngFKPerson)=598 Or (tblSourceDocument.lngFKPerson =0 and tblSourceDocument.lngFKLanguage =0 )) AND ((tblSourceDocument.lngFKSource)=));