{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:20:32Z","timestamp":1740097232895,"version":"3.37.3"},"publisher-location":"Cham","reference-count":10,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319411347"},{"type":"electronic","value":"9783319411354"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41135-4_12","type":"book-chapter","created":{"date-parts":[[2016,6,20]],"date-time":"2016-06-20T12:23:38Z","timestamp":1466425418000},"page":"191-198","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Predicate Testing in Formal Certification"],"prefix":"10.1007","author":[{"given":"Franck","family":"Slama","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,21]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/BFb0020001","volume-title":"Formal Software Development, 4th International Symposium of VDM Europe","author":"J Abrial","year":"1991","unstructured":"Abrial, J., et al.: The B-method. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 398\u2013405. Springer, Heidelberg (1991). http:\/\/dx.doi.org\/ 10.1007\/BFb0020001"},{"key":"12_CR2","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development- Coq\u2019Art","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development- Coq\u2019Art. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). http:\/\/dx.doi.org\/10.1007\/978-3-662-07964-5"},{"key":"12_CR3","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23, 552\u2013593 (2013). http:\/\/journals.cambridge.org\/article_S095679681300018X","journal-title":"J. Funct. Program."},{"issue":"2","key":"12_CR4","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/S1571-0661(04)80508-5","volume":"70","author":"D Delahaye","year":"2002","unstructured":"Delahaye, D.: A proof dedicated meta-language. Electr. Notes Theor. Comput. Sci. 70(2), 96\u2013109 (2002). http:\/\/dx.doi.org\/10.1016\/S1571-0661(04)80508-5","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"5","key":"12_CR5","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"RA DeMillo","year":"1979","unstructured":"DeMillo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. Commun. ACM 22(5), 271\u2013280 (1979). http:\/\/doi.acm.org\/10.1145\/359104.359106","journal-title":"Commun. ACM"},{"key":"12_CR6","unstructured":"Slama, F., Brady, E.: Automatically proving equivalence by type-safe reflection (draft under consideration). J. Funct. Program. (2016). https:\/\/fs39.host.cs.st-andrews.ac.uk\/publications\/paper_Slama_Brady_JFP.pdf"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98\u2013113. Springer, Heidelberg (2005). http:\/\/citeseerx.ist.psu.edu\/viewdoc\/ summary?doi=10.1.1.61.3041"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/978-3-319-08970-6_36","volume-title":"Interactive Theorem Proving","author":"R Krebbers","year":"2014","unstructured":"Krebbers, R., Leroy, X., Wiedijk, F.: Formal C semantics: CompCert and the C standard. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 543\u2013548. Springer, Heidelberg (2014). https:\/\/hal.inria.fr\/hal-00981212"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230\u2013266. Springer, Heidelberg (2009). http:\/\/dx.doi.org\/10.1007\/978-3-642-04652-0_5"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, pp. 87\u2013100, 25\u201327 September 2013. http:\/\/doi.acm.org\/10.1145\/2500365.2500579","DOI":"10.1145\/2544174.2500579"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41135-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T20:13:05Z","timestamp":1568059985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41135-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319411347","9783319411354"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41135-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}