{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T17:47:10Z","timestamp":1743875230127},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642358722"},{"type":"electronic","value":"9783642358739"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35873-9_18","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T06:22:57Z","timestamp":1357107777000},"page":"275-294","source":"Crossref","is-referenced-by-count":46,"title":["Tool Integration with the Evidential Tool Bus"],"prefix":"10.1007","author":[{"given":"Simon","family":"Cruanes","sequence":"first","affiliation":[]},{"given":"Gregoire","family":"Hamon","sequence":"additional","affiliation":[]},{"given":"Sam","family":"Owre","sequence":"additional","affiliation":[]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","volume-title":"Foundations of Databases","author":"S. Abiteboul","year":"1995","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Reading (1995)"},{"doi-asserted-by":"crossref","unstructured":"Alvaro, P., Marczak, W., Conway, N., Hellerstein, J.M., Maier, D., Sears, R.C.: Dedalus: Datalog in Time and Space. Technical report, EECS Department, University of California, Berkeley (December 2009)","key":"18_CR2","DOI":"10.21236\/ADA538767"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"unstructured":"Bloomfield, R.E., Bishop, P.G., Jones, C.C.M., Froome, P.K.D.: Adelard Safety Case Development Manual. Adelard (1998)","key":"18_CR4"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31612-8_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A.R. Bradley","year":"2012","unstructured":"Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 1\u201314. Springer, Heidelberg (2012)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R. Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: An Academic Industrial-Strength Verification Tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 24\u201340. Springer, Heidelberg (2010)"},{"issue":"1","key":"18_CR7","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1109\/69.43410","volume":"1","author":"S. Ceri","year":"1989","unstructured":"Ceri, S., Gottlob, G., Tanca, L.: What you always wanted to know about datalog (and never dared to ask). IEEE Transactions on Knowledge and Data Engineering\u00a01(1), 146\u2013166 (1989)","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C - A Software Analysis Perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-39656-7_9","volume-title":"Formal Methods for Components and Objects","author":"H. Jong de","year":"2003","unstructured":"de Jong, H., Klint, P.: ToolBus: The Next Generation. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 220\u2013241. Springer, Heidelberg (2003)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-46419-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.A. Dennis","year":"2000","unstructured":"Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The PROSPER Toolkit. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 78\u201392. Springer, Heidelberg (2000)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming (2006)","key":"18_CR15","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/978-3-642-28756-5_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Grebenshchikov","year":"2012","unstructured":"Grebenshchikov, S., Gupta, A., Lopes, N.P., Popeea, C., Rybalchenko, A.: HSF(C): A Software Verifier Based on Horn Clauses- (Competition Contribution). In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 549\u2013551. Springer, Heidelberg (2012)"},{"issue":"2","key":"18_CR18","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/s10009-006-0003-0","volume":"9","author":"O. Grumberg","year":"2007","unstructured":"Grumberg, O., Katz, S.: Veritech: a framework for translating among model description notations. STTT\u00a09(2), 119\u2013132 (2007)","journal-title":"STTT"},{"unstructured":"Hallgren, T., Hook, J., Jones, M.P., Kieburtz, R.B.: An overview of the Programatica toolset. In: High Confidence Software and Systems Conference, HCSS 2004 (2004)","key":"18_CR19"},{"unstructured":"Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. In: IEEE Symposium on Logic in Computer Science, Ithaca, NY (1987)","key":"18_CR20"},{"doi-asserted-by":"crossref","unstructured":"Huang, S.S., Green, T.J., Loo, B.T.: Datalog and emerging applications: an interactive tutorial. In: Sellis, T.K., Miller, R.J., Kementsietsidis, A., Velegrakis, Y. (eds.) SIGMOD Conference, pp. 1213\u20131216. ACM (2011)","key":"18_CR21","DOI":"10.1145\/1989323.1989456"},{"issue":"4","key":"18_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R. Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys\u00a041(4), 21:1\u201321:54 (2009)","journal-title":"ACM Computing Surveys"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-02138-1_1","volume-title":"Formal Techniques for Distributed Systems","author":"D. Kitchin","year":"2009","unstructured":"Kitchin, D., Quark, A., Cook, W., Misra, J.: The Orc Programming Language. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol.\u00a05522, pp. 1\u201325. Springer, Heidelberg (2009)"},{"unstructured":"Margaria, T., Nagel, R., Steffen, B.: Remote integration and coordination of verification tools in JETI. In: ECBS, pp. 431\u2013436. IEEE Computer Society (2005)","key":"18_CR24"},{"unstructured":"Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center, Palo Alto, Ca. (1981)","key":"18_CR25"},{"issue":"2","key":"18_CR26","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.: Simplification 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":"18_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002), Isabelle home page: http:\/\/isabelle.in.tum.de\/"},{"key":"18_CR28","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) CADE-16. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-63255-7_33","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"P. Rao","year":"1997","unstructured":"Rao, P., Sagonas, K.F., Swift, T., Warren, D.S., Freire, J.: XSB: A System for Effciently Computing WFS. In: Fuhrbach, U., Dix, J., Nerode, A. (eds.) LPNMR 1997. LNCS, vol.\u00a01265, pp. 430\u2013440. Springer, Heidelberg (1997)"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11576280_3","volume-title":"Formal Methods and Software Engineering","author":"J.M. Rushby","year":"2005","unstructured":"Rushby, J.M.: An Evidential Tool Bus. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 36\u201336. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Wermelinger, M., Gall, H. (eds.) Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2005, Lisbon, Portugal, September 5-9, pp. 263\u2013272. ACM (2005)","key":"18_CR31","DOI":"10.1145\/1081706.1081750"},{"issue":"4","key":"18_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1592434.1592437","volume":"41","author":"N. Shankar","year":"2009","unstructured":"Shankar, N.: Automated deduction for verification. ACM Computing Surveys 41(4), 20:1\u201320:56 (2009)","journal-title":"ACM Computing Surveys"},{"issue":"2-4","key":"18_CR33","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1002\/cpe.938","volume":"17","author":"D. Thain","year":"2005","unstructured":"Thain, D., Tannenbaum, T., Livny, M.: Distributed computing in practice: the Condor experience. Concurrency - Practice and Experience\u00a017(2-4), 323\u2013356 (2005)","journal-title":"Concurrency - Practice and Experience"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35873-9_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,4]],"date-time":"2022-02-04T23:46:39Z","timestamp":1644018399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35873-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642358722","9783642358739"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35873-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}