CSE Colloquium Series
CSE Distinguished Lecture Series
Degree Programs in Computer Science and Engineering @ SMU
Application Forms for Graduate Students
Advice for Graduate Students
Computing Research Association (CRA)
The Collection of Computer Science Bibliographies
Scientific Literature Digital Library (CITESEER)
U.S. Patent Database Page
Conferences Calendar by IEEE & ACM
Turing Awards & Turing Award Lectures
Project Abstracts
Theorem Proving Environments
PVS homepage(PVS Tutorials)Theses
Isabelle/HOL homepage (Tutorial)
VAMP papersKroening, D., Formal Verification of Pipelined Microprocessors, PhD Thesis, University of the Saarland, 2001.
Jacobi, C., Formal Verification of a Fully IEEE Compliant Floating Point Unit, PhD Thesis, University of the Saarland, 2002.
Berg, C., Formal verification of an IEEE floating point adder. Master's thesis, University of the Saarland, May 2001. (pvs-files).
Seidel, P.-M., On the Design and Quantitative Analysis of IEEE Compliant Floatin-Point Units (with correctness proofs), PhD thesis, University of the Saarland, 1999.
Berg, C., Beyer, S., Jacobi, C., Kröning, D., and Leinenbach, D., Formal verification of the VAMP microprocessor (project status). In Proc. Symp. on the Effectiveness of Logic in Computer Science (ELICS02), MPI-I-2002-2-007, pages 31-36, March 2002. (slides) (poster).
Berg, C. and Jacobi, C., Formal verification of the VAMP floating point unit. In CHARME 2001, LNCS 2144, pages 325-339. Springer, Sept. 2001. (slides)
Berg, C., Jacobi, C., and Kroening, D., Formal verification of a basic circuits library. In Applied Informatics 2001, pages 252-255. ACTA Press, February 2001. (slides)
Others
Paul, W.J.. Lecture notes on Formal Computer Architecture I, University of the Saarland, compiled by students in Fall 2001.
Mueller, S.M., Paul, W.J., Computer Architecture - Complexity & Correctness, ISBN 3-540-67481-0, Springer Verlag, 2000.
-->Errata.
References Microprocessor Verification
Algebraic Models of Correctness for Microprocessors
Specification and Verification of Microprocessors in HOLA.C.J. Fox and N.A. Harman, Algebraic Models of Correctness for Microprocessors. Formal Aspects of Computing, 12(4): 298-312, 2000.
A.C.J. Fox An Algebraic Models for Advanced Microprocessors., PhD thesis, University of Wales Swansea, 1998.
Automatic Generation of Invariants in Processor VerificationA.C.J. Fox An Algebraic Framework for Modelling and Verifying Microprocessors Using HOL., 2001.
A.C.J. Fox, A HOL Specification of the ARM Instruction Set Architecture. Technical report No. 545, University of Cambridge Computer Laboratory, June 2001.
A.C.J. Fox, Formal verification of the ARM6 micro-architecture. Technical report No. 548, University of Cambridge Computer Laboratory, November 2002.
Top-level Refinement in Processor VerificationJeffrey X. Su, David L. Dill, Clark W. Barrett, Automatic Generation of Invariants in Processor Verification. First international conference on formal methods in computer-aided design 1996.
Z. Manna, A. Pnueli Temporal Verification of Reactive Systems, Safety. Springer-Verlag, 1995 (p.104-152).
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion FunctionS.Krstic, B.Cook, J.Launchbury, J.Matthews, "Top-level Refinement in Processor Verification", 1998
J.Burch, D.Dill , "Automatic verification of pipelined microprocessor control", 1994.
Specification and Verification of HDL models (2 themes)S. Berezin, E. Clarke, A. Biere, Y. Zhu, "Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function", 2002
S. Berezin, A. Biere, E. Clarke, andY. Zhu, Combining symbolic model checking with uninterpreted functions for out-of-order processor verification, 1998.
Hardware Verification using Monadic Second Order LogicDavid M. Russinoff, Specification and Verification of Gate-Level VHDL Models of Synchronous and Asynchronous Circuits. 1994.
Verification of Synchronous Circuits by Symbolic Logic SimulationDavid A. Basin, Nils Klarrund, Hardware Verification using Monadic Second Order Logic. 1995
A. Aziz, F.Balarin, K.Brayton, A.Sangiovanni-Vincentelli "Sequential Synthesis Using SIS", 2000.
Relative Timing Based Verification of Timed Circuits and SystemsR.E.Bryant, "Verification of Synchronous Circuits by Symbolic Logic Simulation", 1989.
Formal Specification of Abstract Memory Models (Proseminar)H.Kim, P.A.Beerel, K.Stevens "Relative Timing Based Verification of Timed Circuits and Systems", 2001.
David L. Dill and Seungjoon Park and Andreas G. Nowatzyk, "Formal Specification of Abstract Memory Models," Proceedings of the 1993 Symposium, Gaetano Borriello and Carl Ebeling, Eds. MIT Press, 1993, pp 38-52.
Verification of Operating Systems
...
Verification of Compilers
...
Software Verification
Peled, D., Software Reliability Methods, Springer 2001.
Manna, Z. and Pnueli, A., Temporal Verification of Reactive Systems, Springer 1995.
Model Checking
Temporal Logic (summary report: Anton Myagotin
)
Compositional Reasoning (summary report: Ewgenij Filonenko
)
Symmetry (summary report: Elena Petrova
)
Abstraction (summary report: Ramesh Kumar
)
Equivalence Checking
...
Computer Arithmetic
Building the arith.org homepage
Current Graduate Course on Computer Arithmetic
Current Research Projects in CSE8351:
Bibliography
on Computer Arithmetic
Bibliography of Material on Floating-Point Arithmetic
References for Floating-Point on FPGAs
Effective & Adaptive Parallelism
Project Abstracts
Current Projects in CSE5381 &
CSE7381
Undergraduate
Projects:
Graduate
Projects:
+ see
Research Projects in Computer Arithmetic
WWW Computer Architecture Page
PRAM papers & theses
Real
PRAM Programming
...
Computer Graphics Hardware
Abstracts
Hardware Algorithms Applications/Libraries/Benchmarks
2000 SIGGRAPH course by Schneider
Computer Graphics Hardware Conference
Other Conferences on Computer Graphics
Work from Delft, SB, ...
| updated 11/03/03 by
Peter-M. Seidel |
![]() |