{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:39:09Z","timestamp":1725485949607},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414285"},{"type":"electronic","value":"9783540444640"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44464-5_13","type":"book-chapter","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T19:34:00Z","timestamp":1181158440000},"page":"162-181","source":"Crossref","is-referenced-by-count":18,"title":["Reflecting BDDs in Coq"],"prefix":"10.1007","author":[{"given":"Kumar Neeraj","family":"Verma","sequence":"first","affiliation":[]},{"given":"Jean","family":"Goubault-Larrecq","sequence":"additional","affiliation":[]},{"given":"Sanjiva","family":"Prasad","sequence":"additional","affiliation":[]},{"given":"S.","family":"Arun-Kumar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,8]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"S. F. Allen, R. L. Constable, D. J. Howe, and W. E. Aitken. The semantics of reflected proof. In LICS\u201990. IEEE Computer Society Press, June 1990.","DOI":"10.1109\/LICS.1990.113737"},{"key":"13_CR2","unstructured":"B. Barras. Auto-validation d\u2019un syst\u00e8me de preuves avec familles inductives. PhD thesis, University Paris VII, Nov. 1999. Code and Coq proofs available at http:\/\/www.cl.cam.ac.uk\/~bb236\/home\/coq-in-coq.tar.gz."},{"key":"13_CR3","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, H. Laulh\u00e8re, C. Mu\u00f1oz, C. Murthy, C. Parent-Vigouroux, P. Loiseleur, C. Paulin-Mohring, A. Sa\u00efbi, and B. Werner. The Coq proof assistant reference manual. Version 6.2.41, available at http:\/\/coq.inria.fr\/doc\/main.html , Jan. 1999."},{"key":"13_CR4","unstructured":"D. A. Basin and R. Constable. Metalogical frameworks. In G. Huet and G. Plotkin, editors, Logical Environments, pages 1\u201329. Cambridge University Press, 1993. Also available as Technical Report MPI-I-92-205."},{"key":"13_CR5","unstructured":"J.-P. Billon. Perfect normal forms for discrete functions. Technical Report 87019, Bull S. A. Research Center, June 1987."},{"key":"13_CR6","series-title":"Lect Notes Comput Sci","volume-title":"TACS\u201997","author":"S. Boutin","year":"1997","unstructured":"S. Boutin. Using reflection to build efficient and certified decision procedures. In M. Abadi and T. Ito, editors, TACS\u201997. Springer-Verlag LNCS 1281, 1997."},{"key":"13_CR7","unstructured":"R. Boyer and J. S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science, London, 1981. Academic Press."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient implementation of a BDD package. In DAC\u201990. ACM\/IEEE, 1990.","DOI":"10.1145\/123186.123222"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C35(8), Aug. 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"13_CR10","unstructured":"O. Coudert. SIAM: Une Bo\u00eete \u00e0 Outils Pour la Preuve Formelle de Syst\u00e8mes S\u00e9quentiels. PhD thesis, Ecole Nationale Sup\u00e9rieure des T\u00e9l\u00e9communications, Paris, Oct. 1991."},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Types\u201999","author":"H. Goguen","year":"1999","unstructured":"H. Goguen, R. Brooksby, and R. Burstall. Memory management: An abstract formulation of incremental tracing. In Types\u201999. Springer Verlag LNCS, 1999. Submitted."},{"key":"13_CR12","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"G. Gonthier","year":"1996","unstructured":"G. Gonthier. Verifying the safety of a practical concurrent garbage collector. In CAV\u201996. Springer Verlag LNCS 1102, July 1996."},{"key":"13_CR13","unstructured":"M. Gordon. Programming combinations of deduction and BDD-based symbolic calculation. Technical Report 480, University of Cambridge Computer Laboratory, Dec. 1999."},{"key":"13_CR14","unstructured":"M. Gordon and K. F. Larsen. Combining the Hol98 proof assistant with the BuDDy BDD package. Technical Report 481, University of Cambridge Computer Laboratory, Dec. 1999."},{"key":"13_CR15","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"13_CR16","unstructured":"M. J. C. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, a mechanical logic of computation. Report CSR-11-77 (in 2 parts), Dept. of Computer Science, U. Edinburgh, 1977."},{"key":"13_CR17","unstructured":"J. Goubault. Standard ML with fast sets and maps. In ML\u201994. ACM Press, June 1994."},{"key":"13_CR18","unstructured":"J. Goubault-Larrecq. Satisfiability of inequality constraints and detection of cycles with negative weight in graphs. Part of the Coq contribs, available at http:\/\/pauillac.inria.fr\/coq\/contribs\/graphs.html , 1998."},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38, 1995.","DOI":"10.1093\/comjnl\/38.2.162"},{"key":"13_CR20","unstructured":"G. Huet, G. Kahn, and C. Paulin-Mohring. The Coq Proof Assistant, A Tutorial. Coq Project, Inria, 1998. Draft, version 6.2.4. Available at http:\/\/coq.inria.fr\/doc\/tutorial.html."},{"key":"13_CR21","series-title":"Lect Notes Comput Sci","volume-title":"TPHOL\u201998","author":"P. Jackson","year":"1998","unstructured":"P. Jackson. Verifying a garbage collection algorithm. In TPHOL\u201998. Springer Verlag LNCS 1479, 1998."},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"R. Kumar, K. Schneider, and T. Kropf. Structuring and automating hardware proofs in a higher-order theorem-proving environment. Journal of Formal System Design, 1993.","DOI":"10.1007\/BF01383880"},{"key":"13_CR23","unstructured":"Z. Luo and R. Pollack. The LEGO proof development system: A user\u2019s manual. Technical Report ECS-LFCS-92-211, U. of Edinburgh, May 1992."},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. In Functional Programming and Computer Architecture, June 1995.","DOI":"10.1145\/224164.224182"},{"key":"13_CR26","unstructured":"NIST. Common criteria for information technology security evaluation. ISO International Standard (IS) 15408, Jan. 2000. Version 2.1."},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, CADE\u201992. Springer Verlag LNAI 607, June 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"13_CR28","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2, 1986. Errata: Pelletier, Francis Jeffry, JAR 4, pp. 235\u2013236 and Pelletier, Francis Jeffry and Sutcliffe, Geoff, JAR 18(1), p. 135.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"D. M. Russino.. A mechanically verified garbage collector. Formal Aspects of Computing, 6, 1994.","DOI":"10.1007\/BF01211305"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"A. Urquhart. Hard examples for resolution. Journal of the ACM, 34(1), 1987.","DOI":"10.1145\/7531.8928"},{"key":"13_CR31","unstructured":"D. Verkest and L. Claesen. Special benchmark session on tautology checking. In L. Claesen, editor, IMEC-IFIP Workshop on Applied Formal Methods for Correct VLSI Design, 1990."},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"R. W. Weyhrauch. Prolegomena to a theory of mechanized formal reasoning. Artifical Intelligence, 13(1, 2), 1980.","DOI":"10.1016\/0004-3702(80)90015-6"},{"key":"13_CR33","series-title":"Lect Notes Comput Sci","volume-title":"FME\u201997","author":"S. Yu","year":"1997","unstructured":"S. Yu and Z. Luo. Implementing a model checker for LEGO. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME\u201997. Springer-Verlag LNCS 1313, Sept. 1997."}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44464-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:38:37Z","timestamp":1556465917000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44464-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414285","9783540444640"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-44464-5_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}