{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:31:19Z","timestamp":1743150679702,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319212142"},{"type":"electronic","value":"9783319212159"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21215-9_7","type":"book-chapter","created":{"date-parts":[[2015,7,16]],"date-time":"2015-07-16T13:36:34Z","timestamp":1437053794000},"page":"109-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Sequential Generation of Structured Arrays and Its Deductive Verification"],"prefix":"10.1007","author":[{"given":"Richard","family":"Genestier","sequence":"first","affiliation":[]},{"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Petiot","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,17]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Arndt, J.: Matters Computational - Ideas, Algorithms, Source Code [The fxtbook] (2010). http:\/\/www.jjj.de","DOI":"10.1007\/978-3-642-14764-7"},{"key":"7_CR2","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language. http:\/\/frama-c.com\/acsl.html"},{"key":"7_CR3","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Melquiond, G., Paskevich, A.: The Why3 platform 0.81 (March 2013). https:\/\/hal.inria.fr\/hal-00822856"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-35308-6_10","volume-title":"Certified Programs and Proofs","author":"L Bulwahn","year":"2012","unstructured":"Bulwahn, L.: The new Quickcheck for Isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92\u2013108. Springer, Heidelberg (2012)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-14128-7_15","volume-title":"Intelligent Computer Mathematics","author":"F Butelle","year":"2010","unstructured":"Butelle, F., Hivert, F., Mayero, M., Toumazet, F.: Formal proof of SCHUR conjugate function. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 158\u2013171. Springer, Heidelberg (2010)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-32759-9_12","volume-title":"FM 2012: Formal Methods","author":"M Carlier","year":"2012","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: A certified constraint solver over finite domains. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 116\u2013131. Springer, Heidelberg (2012)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. SIGPLAN Not., vol. 35, pp. 268\u2013279. ACM, New York (2000)","DOI":"10.1145\/357766.351266"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-06200-6_17","volume-title":"NASA Formal Methods","author":"L Correnson","year":"2014","unstructured":"Correnson, L.: Qed. computing what remains to be proved. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 215\u2013229. Springer, Heidelberg (2014)"},{"key":"7_CR9","unstructured":"Dijkstra, E.W.: A Discipline of Programming. In: Series in Automatic Computation, Prentice Hall, Englewood Cliffs (1976)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C.: Verifying two lines of C with Why3: an exercise in program verification. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 83\u201397. Springer, Heidelberg (2012). http:\/\/dx.doi.org\/10.1007\/978-3-642-27705-4","DOI":"10.1007\/978-3-642-27705-4_8"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19\u201332. American Mathematical Society, Providence (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering, ICSE 2010, vol. 1, pp. 225\u2013234. ACM, New York (2010)","DOI":"10.1145\/1806799.1806835"},{"issue":"10","key":"7_CR13","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"7_CR14","unstructured":"Marinov, D., Khurshid, S.: TestEra: A novel framework for automated testing of Java programs. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, pp. 22\u201331. IEEE Computer Society, Washington, DC (2001)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Paraskevopoulou, Z., Hri\u0163cu, C.: A Coq framework for verified property based testing (2014). http:\/\/prosecco.gforge.inria.fr\/personal\/hritcu\/publications\/verified-testing-report.pdf","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/978-3-319-09099-3_16","volume-title":"Tests and Proofs","author":"G Petiot","year":"2014","unstructured":"Petiot, G., Kosmatov, N., Giorgetti, A., Julliand, J.: How test generation helps software specification and deductive verification in Frama-C. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 204\u2013211. Springer, Heidelberg (2014)"},{"key":"7_CR17","unstructured":"Ruskey, F.: Combinatorial Generation Working Version (1j-CSC 425\/520) (2003). http:\/\/www.1stworks.com\/ref\/RuskeyCombGen.pdf"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1007\/978-3-662-46669-8_33","volume-title":"Programming Languages and Systems","author":"EL Seidel","year":"2015","unstructured":"Seidel, E.L., Vazou, N., Jhala, R.: Type targeted testing. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 812\u2013836. Springer, Heidelberg (2015)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Sullivan, K.J., Yang, J., Coppit, D., Khurshid, S., Jackson, D.: Software assurance by bounded exhaustive testing. In: Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, pp. 133\u2013142. ACM (July 2004)","DOI":"10.1145\/1007512.1007531"},{"key":"7_CR20","unstructured":"The OEIS Foundation Inc.: The On-Line Encyclopedia of Integer Sequences (2010). http:\/\/oeis.org"},{"issue":"5","key":"7_CR21","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T Weber","year":"2011","unstructured":"Weber, T.: SMT solvers: New oracles for the HOL theorem prover. International Journal on Software Tools for Technology Transfer 13(5), 419\u2013429 (2011)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Williams, N.: Abstract path testing with PathCrawler. In: Proceedings of the 5th Workshop on Automation of Software Test, AST 2010, pp. 35\u201342. ACM, New York (2010)","DOI":"10.1145\/1808266.1808272"},{"key":"7_CR23","unstructured":"Zito, A.: quickcheck4c: A QuickCheck for C (2014). https:\/\/github.com\/nivox\/quickcheck4c"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21215-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T13:04:40Z","timestamp":1676466280000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21215-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319212142","9783319212159"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21215-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"17 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}