| Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D. and Paul, W.J. |
|
EE |
BibTeX |
| Putting it all together - Formal Verification of the VAMP. | | In STTT Journal, Special Issue on Recent Advances in Hardware Verification, | | Springer, 2006. | | | | Jacobi, C. and Berg, C. |
|
EE |
BibTeX |
| Formal Verification of the VAMP Floating Point Unit. | | In Formal Methods in System Design, | | pages 227-266, Springer Netherlands, 2005. | | | | Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D. and Paul, W.J. |
|
EE |
BibTeX |
| Instantiating uninterpreted functional units and memory system: functional verification of the VAMP. | | In Geist, D. and Tronci, E., editors, CHARME 2003, | | volume 2860 of LNCS, pages 51-65, Springer, 2003. | | | | Berg, C. and Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D. |
 |
|
BibTeX |
| Formal Verification of the VAMP Microprocessor (Project Status). | | In Charatonik, Witold and Ganzinger, Harald, editors, Symposium on the Effectiveness of Logic in Computer Science (ELICS02), | | pages 31-36, Max-Planck-Institut für Informatik, 2002. | | | | Jacobi, Christian |
|
|
BibTeX |
| Formal Verification of Complex Out-of-order Pipelines
by Combining Model-Checking and Theorem-Proving. | | In Computer Aided Verification (CAV 02), | | volume 2404 of LNCS, pages 309-323, Springer, 2002. | | | | Beyer, S. and Jacobi, C. and Kroening, D. and Leinenbach, D. |
|
|
BibTeX |
| Correct Hardware by Synthesis from PVS. | | 2002. | | unpublished, available at http://www-wjp.cs.uni-saarland.de/publikationen/BJKL02.pdf | | | | Jacobi, Christian |
|
|
BibTeX |
| Formal Verification of a Fully IEEE Compliant Floating Point Unit. | | | Doktorarbeit, Saarland University, 2002. | | | | Berg, C. and Jacobi, C. and Kröning, D. |
|
|
BibTeX |
| Formal Verification of a Basic Circuits Library. | | In Proc. of the IASTED International Conference on Applied Informatics, Innsbruck (AI 2001), | | Innsbruck, Austria | | ACTA Press, 2001. | | | | Jacobi, Christian |
|
|
BibTeX |
| Formal Verification of a Theory of IEEE Rounding. | | In Boulton, R.J. and Jackson, P.B., editors, TPHOLs 2001: Supplemental Proceedings, | | Edinburgh, UK | | Informatics Research Report EDI-INF-RR-0046, 2001. | | | | Berg, C. and Jacobi, C. |
|
|
BibTeX |
| Formal Verification of the {VAMP} Floating Point Unit. | | In Proc.\ 11th Advanced Research Working Conference on Correct
Hardware Design and Verification Methods ({CHARME}), | | volume 2144 of LNCS, pages 325-339, Springer, 2001. | | | | Jacobi, Christian |
|
|
BibTeX |
| Formal Verification of a Theory of {IEEE} Rounding. | | In Richard J. Boulton and Paul B. Jackson, editors, {TPHOLs} 2001: Supplemental Proceedings.
Informatics Research Report EDI-INF-RR-0046, Univ.
Edinburgh, UK, | | 2001. | | | | Jacobi, C. and Kröning, D. |
|
|
BibTeX |
| Proving the Correctness of a Complete Microprocessor. | | In Mehlhorn, Kurt and Snelting, Gregor, editors, Informatik 2000, Proc. of the 30. Jahrestagung der Gesellschaft für Informatik, | | Informatik aktuell, Springer Verlag, 2000. | | ISBN 3-540-67880-8 | | | | Jacobi, C. and Lichtenau, C. |
|
|
BibTeX |
| Highly Concurrent Locking in Shared Memory Database Systems. | | In Proc. EuroPar 99, | | volume 1685 of Lecture Notes in Computer Science, Springer Verlag, 1999. | | |
|
