{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:31Z","timestamp":1740107971905,"version":"3.37.3"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,6,9]],"date-time":"2017-06-09T00:00:00Z","timestamp":1496966400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000738","name":"University of Leicester","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000738","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10009-017-0460-7","type":"journal-article","created":{"date-parts":[[2017,6,9]],"date-time":"2017-06-09T13:48:42Z","timestamp":1497016122000},"page":"511-515","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Advances in verification presented in TACAS\u201913"],"prefix":"10.1007","volume":"19","author":[{"given":"Nir","family":"Piterman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,9]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In Piterman and Smolka [37], pp. 324\u2013338","key":"460_CR1","DOI":"10.1007\/978-3-642-36742-7_23"},{"doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. Softw. Tools Technol. Transf. (2017, in this issue)","key":"460_CR2","DOI":"10.1007\/s10009-016-0415-4"},{"key":"460_CR3","first-page":"477","volume-title":"Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3\u20137, 2007, Proceedings, Volume 4590 of Lecture Notes in Computer Science","author":"D Amit","year":"2007","unstructured":"Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3\u20137, 2007, Proceedings, Volume 4590 of Lecture Notes in Computer Science, pp. 477\u2013490. Springer, Berlin (2007)"},{"key":"460_CR4","first-page":"99","volume-title":"Model Checking Software\u201420th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings, Volume 7976 of Lecture Notes in Computer Science","author":"JD Backes","year":"2013","unstructured":"Backes, J.D., Person, S., Rungta, N., Tkachuk, O.: Regression verification using impact summaries. In: Bartocci, E., Ramakrishnan, C.R. (eds.) Model Checking Software\u201420th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings, Volume 7976 of Lecture Notes in Computer Science, pp. 99\u2013116. Springer, Berlin (2013)"},{"key":"460_CR5","first-page":"260","volume-title":"Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18\u201322, 2001, Proceedings, Volume 2102 of Lecture Notes in Computer Science","author":"T Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18\u201322, 2001, Proceedings, Volume 2102 of Lecture Notes in Computer Science, pp. 260\u2013264. Springer, Berlin (2001)"},{"issue":"5\u20136","key":"460_CR6","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT 9(5\u20136), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"460_CR7","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Volume 9300 of Lecture Notes in Computer Science","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Volume 9300 of Lecture Notes in Computer Science, pp. 24\u201351. Springer, Berlin (2015)"},{"key":"460_CR8","first-page":"135","volume-title":"Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7\u201314, 2008, Proceedings, Volume 5123 of Lecture Notes in Computer Science","author":"MG Bobaru","year":"2008","unstructured":"Bobaru, M.G., Pasareanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7\u201314, 2008, Proceedings, Volume 5123 of Lecture Notes in Computer Science, pp. 135\u2013148. Springer, Berlin (2008)"},{"key":"460_CR9","first-page":"651","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15\u201317, 2015","author":"A Bouajjani","year":"2015","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15\u201317, 2015, pp. 651\u2013662. ACM, New York (2015)"},{"issue":"6","key":"460_CR10","doi-asserted-by":"crossref","first-page":"26:1","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1\u201326:66 (2011)","journal-title":"J. ACM"},{"unstructured":"Chaki, S., Sharygina, N., Sinha, N.: Verification of evolving software. In: 3rd Workshop on Specification and Verification of Component-Based Systems (2004)","key":"460_CR11"},{"issue":"3","key":"460_CR12","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/s10703-007-0042-5","volume":"32","author":"S Chaki","year":"2008","unstructured":"Chaki, S., Strichman, O.: Three optimizations for assume-guarantee reasoning with $$\\text{ L }^{*}$$ L \u2217 . Formal Methods Syst. Des. 32(3), 267\u2013284 (2008)","journal-title":"Formal Methods Syst. Des."},{"doi-asserted-by":"crossref","unstructured":"Chen, Y.-F., Clarke, E.M., Farzan, A., Tsai, M.-H., Tsay, Y.-K., Wang, B.-Y.: Automated assume-guarantee reasoning through implicit learning. In: Touili et\u00a0al. [40], pp. 511\u2013526","key":"460_CR13","DOI":"10.1007\/978-3-642-14295-6_44"},{"doi-asserted-by":"crossref","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* verification for infinite-state systems. In: Kroening and Pasareanu [29], pp. 13\u201329","key":"460_CR14","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"460_CR15","first-page":"219","volume-title":"ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, June 16\u201319, 2013","author":"B Cook","year":"2013","unstructured":"Cook, B., Koskinen, E.: Reasoning about nondeterminism in programs. In: Boehm, H.-J., Flanagan, C. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, June 16\u201319, 2013, pp. 219\u2013230. ACM, New York (2013)"},{"key":"460_CR16","first-page":"320","volume-title":"Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10\u201313, 2007","author":"B Cook","year":"2007","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10\u201313, 2007, pp. 320\u2013330. ACM, New York (2007)"},{"issue":"5","key":"460_CR17","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88\u201398 (2011)","journal-title":"Commun. ACM"},{"unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.L., Sagiv, M.: Synthesis of circular compositional program proofs via abduction. Softw. Tools Technol. Transf. (2017, in this issue)","key":"460_CR18"},{"doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Sery, O., Sharygina, N.: evolcheck: Incremental upgrade checker for C. In: Piterman and Smolka [37], pp. 292\u2013307","key":"460_CR19","DOI":"10.1007\/978-3-642-36742-7_21"},{"unstructured":"Fedyukovich, G., Sery, O., Sharygina, N.: Flexible sat-based framework for incremental bounded upgrade checking. Softw. Tools Technol. Transf. (2017, in this issue)","key":"460_CR20"},{"doi-asserted-by":"crossref","unstructured":"Ganty, P., Iosif, R., Konecn\u00fd, F.: Underapproximation of procedure summaries for integer programs. In: Piterman and Smolka [37], pp. 245\u2013259","key":"460_CR21","DOI":"10.1007\/978-3-642-36742-7_18"},{"doi-asserted-by":"crossref","unstructured":"Ganty, P., Iosif, R., Konecn\u00fd, F.: Underapproximation of procedure summaries for integer programs. Softw. Tools Technol. Transf. (2017, in this issue)","key":"460_CR22","DOI":"10.1007\/s10009-016-0420-7"},{"key":"460_CR23","first-page":"112","volume-title":"Static Analysis\u201418th International Symposium, SAS 2011, Venice, Italy, September 14\u201316, 2011. Proceedings, Volume 6887 of Lecture Notes in Computer Science","author":"P Godefroid","year":"2011","unstructured":"Godefroid, P., Lahiri, S.K., Rubio-Gonz\u00e1lez, C.: Statically validating must summaries for incremental compositional dynamic test generation. In: Yahav, E. (ed.) Static Analysis\u201418th International Symposium, SAS 2011, Venice, Italy, September 14\u201316, 2011. Proceedings, Volume 6887 of Lecture Notes in Computer Science, pp. 112\u2013128. Springer, Berlin (2011)"},{"unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2008, San Diego, California, USA, 10th February\u201313th February 2008. The Internet Society (2008)","key":"460_CR24"},{"key":"460_CR25","first-page":"466","volume-title":"Proceedings of the 46th Design Automation Conference, DAC 2009, San Francisco, CA, USA, July 26\u201331, 2009","author":"B Godlin","year":"2009","unstructured":"Godlin, B., Strichman, O.: Regression verification. Proceedings of the 46th Design Automation Conference, DAC 2009, San Francisco, CA, USA, July 26\u201331, 2009, pp. 466\u2013471. ACM, New York (2009)"},{"doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening and Pasareanu [29], pp. 343\u2013361","key":"460_CR26","DOI":"10.1007\/978-3-319-21690-4_20"},{"issue":"3","key":"460_CR27","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"460_CR28","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016)","journal-title":"Formal Methods Syst. Des."},{"volume-title":"Computer Aided Verification\u201327th International Conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part I, Volume 9206 of Lecture Notes in Computer Science","year":"2015","unstructured":"Kroening, D., Pasareanu, C.S. (eds.): Computer Aided Verification\u201327th International Conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part I, Volume 9206 of Lecture Notes in Computer Science. Springer, Berlin (2015)","key":"460_CR29"},{"key":"460_CR30","first-page":"345","volume-title":"Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC\/FSE\u201913, Saint Petersburg, Russian Federation, August 18\u201326, 2013","author":"SK Lahiri","year":"2013","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Meyer, B., Baresi, L., Mezini, M. (eds.) Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC\/FSE\u201913, Saint Petersburg, Russian Federation, August 18\u201326, 2013, pp. 345\u2013355. ACM, New York (2013)"},{"doi-asserted-by":"crossref","unstructured":"Li, B., Dillig, I., Dillig, T., McMillan, K.L., Sagiv, M.: Synthesis of circular compositional program proofs via abduction. In: Piterman and Smolka [37], pp. 370\u2013384","key":"460_CR31","DOI":"10.1007\/978-3-642-36742-7_26"},{"key":"460_CR32","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/978-3-642-05089-3_21","volume-title":"FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2\u20136, 2009. Proceedings, Volume 5850 of Lecture Notes in Computer Science","author":"Y Liu","year":"2009","unstructured":"Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: Cavalcanti, A., Dams, D. (eds.) FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2\u20136, 2009. Proceedings, Volume 5850 of Lecture Notes in Computer Science, pp. 321\u2013337. Springer, Berlin (2009)"},{"key":"460_CR33","first-page":"123","volume-title":"Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17\u201320, 2006, Proceedings, Volume 4144 of Lecture Notes in Computer Science","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17\u201320, 2006, Proceedings, Volume 4144 of Lecture Notes in Computer Science, pp. 123\u2013136. Springer, Berlin (2006)"},{"key":"460_CR34","first-page":"85","volume-title":"Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, PODC 2010, Zurich, Switzerland, July 25\u201328, 2010","author":"PW O\u2019Hearn","year":"2010","unstructured":"O\u2019Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: Richa, A.W., Guerraoui, R. (eds.) Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, PODC 2010, Zurich, Switzerland, July 25\u201328, 2010, pp. 85\u201394. ACM, New York (2010)"},{"issue":"5","key":"460_CR35","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"issue":"3","key":"460_CR36","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"CS Pasareanu","year":"2008","unstructured":"Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the l* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175\u2013205 (2008)","journal-title":"Formal Methods Syst. Des."},{"doi-asserted-by":"crossref","unstructured":"Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201419th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science. Springer, Berlin (2013)","key":"460_CR37","DOI":"10.1007\/978-3-642-36742-7"},{"key":"460_CR38","volume-title":"In Transition from Global to Modular Temporal Reasoning About Programs","author":"A Pnueli","year":"1985","unstructured":"Pnueli, A.: In Transition from Global to Modular Temporal Reasoning About Programs. Springer, Berlin (1985)"},{"key":"460_CR39","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/11526841_34","volume-title":"FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18\u201322, 2005, Proceedings, Volume 3582 of Lecture Notes in Computer Science","author":"N Sharygina","year":"2005","unstructured":"Sharygina, N., Chaki, S., Clarke, E.M., Sinha, N.: Dynamic component substitutability analysis. In: Fitzgerald, J.S., Hayes, I.J., Andrzej, T. (eds.) FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18\u201322, 2005, Proceedings, Volume 3582 of Lecture Notes in Computer Science, pp. 512\u2013528. Springer, Berlin (2005)"},{"doi-asserted-by":"crossref","unstructured":"Touili, T., Cook, B., Jackson, P.B. (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15\u201319, 2010. Proceedings, Volume 6174 of Lecture Notes in Computer Science. Springer, Berlin (2010)","key":"460_CR40","DOI":"10.1007\/978-3-642-14295-6"},{"key":"460_CR41","first-page":"335","volume-title":"Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18\u201320, 2009. Proceedings, Volume 5403 of Lecture Notes in Computer Science","author":"V Vafeiadis","year":"2009","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18\u201320, 2009. Proceedings, Volume 5403 of Lecture Notes in Computer Science, pp. 335\u2013348. Springer, Berlin (2009)"},{"doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili et\u00a0al. [40], pp. 450\u2013464","key":"460_CR42","DOI":"10.1007\/978-3-642-14295-6_40"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0460-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0460-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0460-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T12:03:46Z","timestamp":1659096226000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0460-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,9]]},"references-count":42,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["460"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0460-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2017,6,9]]}}}