{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:27:49Z","timestamp":1725794869003},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662436516"},{"type":"electronic","value":"9783662436523"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43652-3_27","type":"book-chapter","created":{"date-parts":[[2014,5,29]],"date-time":"2014-05-29T02:22:12Z","timestamp":1401330132000},"page":"294-297","source":"Crossref","is-referenced-by-count":4,"title":["Tuning the Alt-Ergo SMT Solver for B Proof Obligations"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Conchon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Iguernelala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-22438-6_14","volume-title":"Automated Deduction \u2013 CADE-23","author":"G. Burel","year":"2011","unstructured":"Burel, G.: Experimenting with Deduction Modulo. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 162\u2013176. Springer, Heidelberg (2011)"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Conchon, S., Contejean, E., Iguernelala, M.: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories: Design and Implementation. Logical Methods in Computer Science\u00a08(3) (2012)","DOI":"10.2168\/LMCS-8(3:16)2012"},{"issue":"2","key":"27_CR3","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.entcs.2008.04.080","volume":"198","author":"S. Conchon","year":"2008","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): Semantic Combination of Congruence Closure with Solvable Theories. Electronic Notes in Theoretical Computer Science\u00a0198(2), 51\u201369 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"27_CR4","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. In: International Workshop on the Implementation of Logics (IWIL), Stellenbosch (South Africa). EasyChair (December 2013) (to appear)"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-45221-5_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Delahaye","year":"2013","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol.\u00a08312, pp. 274\u2013290. Springer, Heidelberg (2013)"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J.-C. Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 Where Programs Meet Provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-30885-7_17","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D. Mentr\u00e9","year":"2012","unstructured":"Mentr\u00e9, D., March\u00e9, C., Filli\u00e2tre, J.-C., Asuka, M.: Discharging Proof Obligations from Atelier\u00a0B Using Multiple Automated Provers. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol.\u00a07316, pp. 238\u2013251. Springer, Heidelberg (2012)"},{"key":"27_CR8","unstructured":"The Bware Project (2012), \n                  \n                    http:\/\/bware.lri.fr\/"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43652-3_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T23:05:59Z","timestamp":1558911959000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43652-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436516","9783662436523"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43652-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}