{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:33Z","timestamp":1762458873544},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642182747"},{"type":"electronic","value":"9783642182754"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-18275-4_20","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T05:06:38Z","timestamp":1295240798000},"page":"278-293","source":"Crossref","is-referenced-by-count":15,"title":["Towards Complete Reasoning about Axiomatic Specifications"],"prefix":"10.1007","author":[{"given":"Swen","family":"Jacobs","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified SMT formulas. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: International Conference on Software Engineering, ICSE (2010)","DOI":"10.1145\/1806799.1806835"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-02658-4_29","volume-title":"Computer Aided Verification","author":"S. Jacobs","year":"2009","unstructured":"Jacobs, S.: Incremental instance generation in local reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 368\u2013382. Springer, Heidelberg (2009)"},{"key":"20_CR7","unstructured":"Jacobs, S.: Hierarchic Decision Procedures for Verification. PhD thesis, Saarland University, Germany (2010)"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Kuncak, V.: On complete reasoning about axiomatic specifications. Technical Report EPFL-REPORT-151486, EPFL (2010)","DOI":"10.1007\/978-3-642-18275-4_20"},{"issue":"8","key":"20_CR9","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2006.11.038","volume":"174","author":"S. Jacobs","year":"2007","unstructured":"Jacobs, S., Sofronie-Stokkermans, V.: Applications of hierarchical reasoning in the verification of complex systems. Electronic Notes in Theoretical Computer Science\u00a0174(8), 39\u201354 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-540-30579-8_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Lam","year":"2005","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking for data structure consistency. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 430\u2013447. Springer, Heidelberg (2005)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Podelski, A., Wies, T.: Counterexample-guided focus. In: 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (2010)","DOI":"10.1145\/1706299.1706330"},{"key":"20_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"20_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-85845-4_17","volume-title":"KI 2008: Advances in Artificial Intelligence","author":"V. Sofronie-Stokkermans","year":"2008","unstructured":"Sofronie-Stokkermans, V.: Efficient hierarchical reasoning about functions over numerical domains. In: Dengel, A.R., Berns, K., Breuel, T.M., Bomarius, F., Roth-Berghofer, T.R. (eds.) KI 2008. LNCS (LNAI), vol.\u00a05243, pp. 135\u2013143. Springer, Heidelberg (2008)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-02959-2_5","volume-title":"Automated Deduction \u2013 CADE-22","author":"V. Sofronie-Stokkermans","year":"2009","unstructured":"Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 67\u201383. Springer, Heidelberg (2009)"},{"issue":"4-6","key":"20_CR16","first-page":"397","volume":"13","author":"V. Sofronie-Stokkermans","year":"2007","unstructured":"Sofronie-Stokkermans, V., Ihlemann, C.: Automated reasoning in some local extensions of ordered structures. Journal of Multiple-Valued Logic and Soft Computing\u00a013(4-6), 397\u2013414 (2007)","journal-title":"Journal of Multiple-Valued Logic and Soft Computing"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (2010)","DOI":"10.1145\/1706299.1706325"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/11609773_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Wies","year":"2005","unstructured":"Wies, T., Kuncak, V., Lam, P., Podelski, A., Rinard, M.: Field constraint analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 157\u2013173. Springer, Heidelberg (2005)"},{"key":"20_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-25984-8_9","volume-title":"Automated Reasoning","author":"T. Zhang","year":"2004","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for recursive data structures with integer constraints. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 152\u2013167. Springer, Heidelberg (2004)"}],"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-18275-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T22:39:30Z","timestamp":1559947170000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}