BibSonomy :: author  ::

bookmarks

publications

(134)

• Automatic Abstraction in Symbolic Trajectory Evaluation.
  Sara Adams and Magnus Björk and Thomas F. Melham and Carl-Johan H. Seger FMCAD 127-135 (2007)
  to dblp by dblp on 2008-02-11 00:00:00
  | URL | BibTeX  
• A reflective functional language for hardware design and theorem proving.
  Jim Grundy and Thomas F. Melham and John W. O'Leary J. Funct. Program. 16 157-196 (2006)
  to dblp by dblp on 2007-02-20 00:00:00
  | URL | BibTeX  
• On the Correctness of Operating System Kernels.
  Mauro Gargano and Mark A. Hillebrand and Dirk Leinenbach and Wolfgang J. Paul TPHOLs 1-16 (2005)
  to dblp by dblp on 2006-05-03 00:00:00
  | URL | BibTeX  
• An industrially effective environment for formal hardware verification.
  Carl-Johan H. Seger and Robert B. Jones and John W. O'Leary and Thomas F. Melham and Mark Aagaard and Clark Barrett and Don Syme IEEE Trans. on CAD of Integrated Circuits and Systems 24 1381-1405 (2005)
  to dblp by dblp on 2006-04-19 00:00:00
  | URL | BibTeX  
• Tool Building Requirements for an API to First-Order Solvers.
  Jim Grundy and Thomas F. Melham and Sava Krstic and Sean McLaughlin Electr. Notes Theor. Comput. Sci. 144 15-26 (2006)
  to dblp by dblp on 2006-02-20 00:00:00
  | URL | BibTeX  
• Formal Verification of the VAMP Floating Point Unit.
  Christoph Berg and Christian Jacobi CHARME 325-339 (2001)
  to dblp by dblp on 2006-02-13 00:00:00
  | URL | BibTeX  
• Proof Pearl: A Formal Proof of Higman's Lemma in ACL2.
  Francisco-Jesús Martín-Mateos and José-Luis Ruiz-Reina and José-Antonio Alonso and María-José Hidalgo TPHOLs 358-372 (2005)
  to dblp by dblp on 2006-01-03 00:00:00
  | URL | BibTeX  
• Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming.
  Xuandong Li and Pei Yu and Jianhua Zhao and Yong Li and Tao Zheng and Guoliang Zheng CHARME 465-480 (2001)
  to dblp by dblp on 2005-12-20 00:00:00
  | URL | BibTeX  
• A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.
  Tom Ridge and James Margetson TPHOLs 294-309 (2005)
  to dblp by dblp on 2005-09-15 00:00:00
  | URL | BibTeX  
• Proof Pearl: Defining Functions over Finite Sets.
  Tobias Nipkow and Lawrence C. Paulson TPHOLs 385-396 (2005)
  to dblp by dblp on 2005-09-15 00:00:00
  | URL | BibTeX