{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T23:47:23Z","timestamp":1757548043104},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642308840"},{"type":"electronic","value":"9783642308857"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30885-7_14","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:50:45Z","timestamp":1340787045000},"page":"194-207","source":"Crossref","is-referenced-by-count":35,"title":["SMT Solvers for Rodin"],"prefix":"10.1007","author":[{"given":"David","family":"D\u00e9harbe","sequence":"first","affiliation":[]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[]},{"given":"Yoann","family":"Guyot","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Voisin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M. Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"14_CR3","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, ch. 26, pp. 825\u2013885. IOS Press (February 2009)"},{"key":"14_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard Version\u00a02.0 (2010)"},{"key":"14_CR5","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T. Bouton","year":"2009","unstructured":"Bouton, T., de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: An Open, Trustable and Efficient SMT-Solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 151\u2013156. Springer, Heidelberg (2009)"},{"key":"14_CR7","unstructured":"Coleman, J., Jones, C., Oliver, I., Romanovsky, A., Troubitsyna, E.: RODIN (Rigorous open Development Environment for Complex Systems). In: Fifth European Dependable Computing Conference: EDCC-5 supplementary volume, pp. 23\u201326 (2005)"},{"key":"14_CR8","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1590\/S0104-65002003000300003","volume":"9","author":"J.-F. Couchot","year":"2003","unstructured":"Couchot, J.-F., D\u00e9harbe, D., Giorgetti, A., Ranise, S.: Scalable Automated Proving and Debugging of Set-Based Specifications. Journal of the Brazilian Computer Society\u00a09, 17\u201336 (2003)","journal-title":"Journal of the Brazilian Computer Society"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-11811-1_17","volume-title":"Abstract State Machines, Alloy, B and Z","author":"D. D\u00e9harbe","year":"2010","unstructured":"D\u00e9harbe, D.: Automatic Verification for a Class of Proof Obligations with SMT-Solvers. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 217\u2013230. Springer, Heidelberg (2010)"},{"key":"14_CR11","unstructured":"D\u00e9harbe, D.: Integration of SMT-solvers in B and Event-B development environments. Science of Computer Programming (March 2011)"},{"key":"14_CR12","unstructured":"Konrad, M., Voisin, L.: Translation from Set-Theory to Predicate Calculus. Technical report, ETH Zurich (2011)"},{"key":"14_CR13","unstructured":"Kr\u00f6ning, D., R\u00fcmmer, P., Weissenbacher, G.: A Proposal for a Theory of Finite Sets, Lists, and Maps for the SMT-LIB Standard. In: Informal proceedings, 7th Int\u2019l Workshop on Satisfiability Modulo Theories (SMT) at CADE 22 (2009)"},{"key":"14_CR14","unstructured":"M\u00e9tayer, C., Voisin, L.: The Event-B mathematical language (2009), \n                    \n                      http:\/\/deploy-eprints.ecs.soton.ac.uk\/11\/4\/kernel_lang.pdf"},{"issue":"2","key":"14_CR15","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplifications by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR16","unstructured":"Schmalz, M.: The logic of Event-B, Technical report 698, ETH Z\u00fcrich, Information Security (2011)"},{"issue":"2\/3","key":"14_CR17","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E - A Brainiac Theorem Prover. AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"AI Communications"},{"key":"14_CR18","unstructured":"The Eclipse Foundation. Eclipse SDK (2009)"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems (FroCoS), Applied Logic, pp. 103\u2013120. Kluwer Academic Publishers (March 1996)","DOI":"10.1007\/978-94-009-0349-4_5"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30885-7_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:33:08Z","timestamp":1620127988000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30885-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642308840","9783642308857"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30885-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}