{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:39:05Z","timestamp":1742913545709,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642156427"},{"type":"electronic","value":"9783642156434"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-15643-4_32","type":"book-chapter","created":{"date-parts":[[2010,9,20]],"date-time":"2010-09-20T09:39:39Z","timestamp":1284975579000},"page":"387-395","source":"Crossref","is-referenced-by-count":1,"title":["COMBINE: A Tool on Combined Formal Methods for Bindingly Verification"],"prefix":"10.1007","author":[{"given":"An N.","family":"Nguyen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tho T.","family":"Quan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phung H.","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thang H.","family":"Bui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M., et al.: Formal methods: State of the art and future directions. ACM Survey\u00a028, 626\u2013643 (1996)","journal-title":"ACM Survey"},{"key":"32_CR2","volume-title":"Principles of Automated Theorem Proving","author":"D.A. Duffy","year":"1991","unstructured":"Duffy, D.A.: Principles of Automated Theorem Proving. John Wiley & Sons, Chichester (1991)"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: Conference Record for of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 191\u2013202 (2002)","DOI":"10.1145\/565816.503291"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs, 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"32_CR5","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, preliminary design (version 1.4) (October 2008)"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Mcpeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: International Conference on Compiler Construction, pp. 213\u2013228 (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Quan, T.T., Hoang, D.L.N., Nguyen, B.T., Nguyen, A.N., Tran, Q.D., Nguyen, P.H., Bui, T.H., et al.: MAFSE: A model-based framework for software verification. In: Proceedings of the 4th International Conference on Secure Software Integration and Reliability Improvement, Singapore (2010)","DOI":"10.1109\/SSIRI-C.2010.36"},{"key":"32_CR8","unstructured":"Quan, T.T., Hoang, D.L.N., Nguyen, V.H., Nguyen, P.H.: Model\u2013based Generation of Structured Error\u2013Flows in Imperative Programs. In: Proceedings of International Conference on Advanced Computing and Applications (ACOMP 2010), Vietnam (2010)"},{"key":"32_CR9","unstructured":"Z3: An Efficient SMT Solver, \n                    \n                      http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/"},{"key":"32_CR10","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking, Tehcnical report, \n                    \n                      http:\/\/www.hpl.hp.com\/techreports\/2003\/HPL-2003-148.html"},{"key":"32_CR11","unstructured":"The Alt-Ergo Theorem Prover, \n                    \n                      http:\/\/alt-ergo.lri.fr\/"},{"key":"32_CR12","unstructured":"Frama-C, \n                    \n                      http:\/\/frama-c.com\/"},{"key":"32_CR13","unstructured":"Jessie plugin, \n                    \n                      http:\/\/frama-c.cea.fr\/jessie.html"},{"key":"32_CR14","unstructured":"Spin \u2013 Formal Verification, \n                    \n                      http:\/\/spinroot.com\/"},{"key":"32_CR15","unstructured":"The Coq Proof Assistant, \n                    \n                      http:\/\/www.lix.polytechnique.fr\/coq\/"},{"key":"32_CR16","unstructured":"Isabelle, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/"},{"key":"32_CR17","unstructured":"Redlog, \n                    \n                      http:\/\/redlog.dolzmann.de\/"},{"key":"32_CR18","unstructured":"Why: a software verification platform, \n                    \n                      http:\/\/why.lri.fr\/"},{"key":"32_CR19","unstructured":"HIP Overview, \n                    \n                      http:\/\/loris-7.ddns.comp.nus.edu.sg\/~project\/hip\/index.html."},{"key":"32_CR20","unstructured":"Java PathFinder, \n                    \n                      http:\/\/babelfish.arc.nasa.gov\/trac\/jpf"},{"key":"32_CR21","unstructured":"NuSMV \u2013 a new symbolic model checker, \n                    \n                      http:\/\/nusmv.fbk.eu\/"},{"key":"32_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"CAV 2009","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)"},{"key":"32_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002: Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"Flanagan, C.: Hybrid type checking. In: POPL 2006: Principles of Programming Languages, pp. 245\u2013256 (2006)","DOI":"10.1145\/1111320.1111059"},{"key":"32_CR25","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, pp. 268\u2013279 (2000)","DOI":"10.1145\/357766.351266"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15643-4_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:57:43Z","timestamp":1558292263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15643-4_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642156427","9783642156434"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15643-4_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}