{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,9]],"date-time":"2024-07-09T17:16:40Z","timestamp":1720545400029},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2004,11,1]],"date-time":"2004-11-01T00:00:00Z","timestamp":1099267200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2004,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We investigate how to take advantage of the particular features of the calculus of inductive constructions in the framework of hardware verification. First, we emphasize in a short case study the use of dependent types and of the constructive aspect of the logic for specifying and synthesizing combinatorial circuits. Then, co-inductive types are introduced to model the temporal aspects of sequential synchronous devices. Moore and Mealy automata are co-inductively axiomatized and are used to represent uniformly both the structures and the behaviors of the circuits. This leads to clear, general and elegant proof processes as is illustrated on the example of a realistic circuit: the ATM Switch Fabric. All the proofs are carried out using Coq.<\/jats:p>","DOI":"10.1007\/s00165-004-0048-3","type":"journal-article","created":{"date-parts":[[2004,6,24]],"date-time":"2004-06-24T05:50:27Z","timestamp":1088056227000},"page":"352-373","source":"Crossref","is-referenced-by-count":10,"title":["Certifying circuits in Type Theory"],"prefix":"10.1145","volume":"16","author":[{"given":"Solange","family":"Coupet-Grimal","sequence":"first","affiliation":[{"name":"Laboratoire d\u2019Informatique Fondamentale de Marseille (UMR 6166), CMI, Universit\u00e9 de Provence, 39 rue Joliot-Curie, F-13453, Marseille, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Line","family":"Jakubiec","sequence":"additional","affiliation":[{"name":"Facult\u00e9 des Sciences de Luminy, Universit\u00e9 de la M\u00e9diterran\u00e9e, 163 Avenue de Luminy, 13288, Marseille Cedex-9"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"LPAR","author":"Boulm\u00e9 S","year":"2001"},{"key":"p_2","volume-title":"Sequential machines and automata theory","author":"Boo TL","year":"1967"},{"key":"p_3","article-title":"Graph-based algorithms for boolean function manipulations","author":"Bry R","year":"1986","journal-title":"IEEE Trans Comput C-35(8):677-691"},{"key":"p_4","volume-title":"The 1996 international conference on theorem proving in higher order logics, TPHOL'96, Turku. Springer, Berlin Heidelberg New York","author":"Coupet-Grimal S","year":"1996"},{"key":"p_5","volume-title":"EUROCAL 85, Linz, LNCS, vol 203","author":"Coquand T","year":"1985"},{"key":"p_6","volume-title":"Verification and synthesis of hardware linear arithmetic structures: the Coq users's contributions","author":"Ja S","year":"1996"},{"key":"p_7","volume-title":"Verification of sequential synchronous circuits","author":"Jb S","year":"2000"},{"key":"p_8","volume-title":"TPHOLs'99, LNCS, vol 1690. Nice","author":"Coupet-Grimal S","year":"1999"},{"key":"p_9","first-page":"183","volume-title":"Proceedings of the 9th annual IEEE conference on computer assurance. IEEE Press","author":"Cur P","year":"1994"},{"key":"p_10","volume-title":"The formal verification of the fairisle ATM switching element. Technical report 329","author":"Cur P","year":"1994"},{"key":"p_11","volume-title":"Ecole Normale Sup\u00e9rieure de Lyon","author":"Gim E","year":"1996"},{"key":"p_12","volume-title":"IX Brazilian symposium on the design of integrated circuits","author":"Garcez E","year":"1996"},{"key":"p_13","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1098\/rsta.1992.0029","article-title":"Dependent types and formal synthesis","volume":"339","author":"Hanna FK","year":"1992","journal-title":"Philos Trans R Soc Lond"},{"issue":"9","key":"p_14","doi-asserted-by":"crossref","first-page":"949","DOI":"10.1109\/32.58783","article-title":"Specification and verification using dependent types","volume":"16","author":"Hanna FK","year":"1990","journal-title":"IEEE Trans Software Eng"},{"key":"p_15","volume-title":"Introduction to automata theory, languages and computation","author":"Hopcroft L","year":"1979"},{"key":"p_16","volume-title":"Universit\u00e9 de Provence, Juillet","author":"Jak L","year":"1999"},{"key":"p_17","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/s10009-002-0082-5","article-title":"Hierarchical formal verification using a hybrid tool","volume":"4","author":"Kort S","year":"2003","journal-title":"Int J Software Tools Technol Transfer"},{"key":"p_18","volume-title":"http:\/\/www.cs.chalmers.se\/\u223ckoen\/Lava","author":"Lav","year":"2000"},{"key":"p_19","series-title":"International series on computer science","first-page":"49","volume-title":"Hoare CAR, Gordon MJC (eds) Mechanized reasoning and hardware design","author":"Lee M","year":"1992"},{"key":"p_20","volume-title":"Fairisle: a general topology ATM LAN","author":"Leslie IM","year":"1990"},{"issue":"19","key":"p_21","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1145\/115994.116022","article-title":"Fairisle: an ATM network for the local area","volume":"4","author":"Leslie IM","year":"1991","journal-title":"ACM Commun Rev"},{"key":"p_22","first-page":"368","volume-title":"Lafayette. IEEE Computer Society Press","author":"Lu J","year":"1998"},{"issue":"5","key":"p_23","doi-asserted-by":"crossref","first-page":"1045","DOI":"10.1002\/j.1538-7305.1955.tb03788.x","article-title":"A method for synthesizing sequential circuits","volume":"34","author":"Mea GH","year":"1955","journal-title":"Bell Syst Techn J"},{"key":"p_24","volume-title":"Designing correct circuits, B\u00e5stad","author":"Miner PS","year":"1996"},{"key":"p_25","first-page":"129","volume-title":"Shannon CE, McCarthy J (eds) Automata studies","author":"Moo EF","year":"1956"},{"key":"p_26","volume-title":"Juillet","author":"Paulin-Mohring C","year":"1995"},{"key":"p_27","volume-title":"Universit\u00e9 Claude Bernard Lyon I","author":"Paulin-Mohring C","year":"1996"},{"key":"p_28","first-page":"89","volume-title":"Alves-Foss J (ed) International workshop on higher order logic theorem proving and its applications: B-track: short presentation","author":"Schneider K","year":"1995"},{"key":"p_29","first-page":"415","volume-title":"Grundy J, Von Wright J, Harrison J (eds) In: TPHOLs'96, Turku (Finlande), LNCS, vol 1125","author":"Tahar S","year":"1996"},{"issue":"4","key":"p_30","first-page":"372","article-title":"Comparing HOL and MDG: a case study on the verification of an ATM switch fabric","volume":"6","author":"Tahar S","year":"1999","journal-title":"Nord J Comput"},{"key":"p_31","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/3-540-49519-3_28","volume-title":"MDG and VIS compared. In: Gopalakrishnan G, Windley P (eds) Formal methods in computer-aided design","author":"Tahar S","year":"1998"},{"key":"p_32","volume-title":"LogiCal Project-INRIA","author":"Tea","year":"2001"},{"issue":"7","key":"p_33","doi-asserted-by":"crossref","first-page":"956","DOI":"10.1109\/43.771178","article-title":"Modeling and verification of the Fairisle ATM switch fabric using MDGs","volume":"18","author":"Tahar S","year":"1999","journal-title":"IEEE Trans CAD Integrated Circuits Syst"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0048-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0048-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0048-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:46:53Z","timestamp":1641484013000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0048-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,11]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,11]]}},"alternative-id":["10.1007\/s00165-004-0048-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0048-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,11]]}}}