INRIA
- UR
Sophia-Antipolis
2004, route des Lucioles
BP 93
06902 Sophia-Antipolis Cedex
FRANCE
Telephone: (33) 04 92 38 79 45
Fax:(33) 04 92 38 76 44
e-mail : Line.Jakubiec@sophia.inria.fr
Telephone: (33) 04 91 11 36 19
Fax: (33) 04 91 11 36 02
e-mail : Line.Jakubiec@lim.univ-mrs.fr
Publications :
[1] Verification de circuits dans Coq (L. Jakubiec)
PhD Thesis (Universite de
Provence - LIM)
July 1999
Postscript document : these.ps
Annexe (Coq
files) : annexe.ps.gz
[2] Hardware Verification using Co-induction in Coq
(S. Coupet-Grimal, L. Jakubiec)
In TPHOL'99, Series LNCS
1690 (pages 91-108)
Y. Bertot, G. Dowek, A. Hirschowitz,
C.Paulin, L.Thery, editors
Nice, France (Sep. 1999)
Postscript : tphol99.ps
[3] Specifications of the ATM Switch Fabric in Coq (L.
Jakubiec)
Research Report LIM
RR1997.234 (May 1997)
Postscript : ATM.ps
[4] A Comparison of the Coq and HOL Proof Systems for Specifying
Hardware (L. Jakubiec, S. Coupet-Grimal, P. Curzon)
Supplementary Proceeding
of TPHOLs'97 (pages 63-78)
E. L. Gunter and A. Felty,
editors
Murray Hill, NJ, USA (Aug.
1997)
Postscript : tphol97.ps
[5] Coq and Hardware Verification : a Case Study
(S. Coupet-Grimal, L. Jakubiec)
In TPHOL'96 , Series LNCS
1125 (pages 125-139)
J. Grundy, J. Von Wright,
J. Harrison, editors
Turku, Finlande (Aug. 1996)
Postscript : tphol96.ps
[6] A System for Modelling and Proving Circuits (M. Allemand,
S. Coupet-Grimal, L. Jakubiec, J-L. Paillet)
EDTC'96 (IEEE European
Design and Test Conference and Exhibition), Paris
March 1996
Postscript : etcd96.ps
[7] Verification formelle de circuits avec Coq (L.
Jakubiec)
Master's thesis (Universite
de Provence)
July 1994
------------------------------------------------------------------------------