{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:39:35Z","timestamp":1777347575670,"version":"3.51.4"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319980461","type":"print"},{"value":"9783319980478","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98047-8_13","type":"book-chapter","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T21:05:49Z","timestamp":1540328749000},"page":"203-219","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The Binomial Heap Verification Challenge in Viper"],"prefix":"10.1007","author":[{"given":"Peter","family":"M\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"S. Blom, S. Darabi, M. Huisman, and W. Oortwijn. The VerCors tool set: Verification of parallel and concurrent software. In N. Polikarpova and S. Schneider, editors, Integrated Formal Methods (IFM), volume 10510 of LNCS, pages 102\u2013110. Springer, 2017.","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"J. Boyland. Checking interference with fractional permissions. In Static Analysis Symposium (SAS), volume 2694 of LNCS, pages 55\u201372. Springer, 2003.","DOI":"10.1007\/3-540-44898-5_4"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"C. Calcagno, D. Distefano, P. W. O\u2019Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. In Z. Shao and B. C. Pierce, editors, Principles of Programming Languages (POPL), pages 289\u2013300. ACM, 2009.","DOI":"10.1145\/1594834.1480917"},{"key":"13_CR4","unstructured":"T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms, 3rd Edition. MIT Press, 2009."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"M. Doko and V. Vafeiadis. Tackling real-life relaxed concurrency with FSL++. In H. Yang, editor, European Symposium on Programming (ESOP), volume 10201 of LNCS, pages 448\u2013475. Springer, 2017.","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. T. V. Setty, and B. Zill. Ironfleet: proving practical distributed systems correct. In E. L. Miller and S. Hand, editors, Symposium on Operating Systems Principles (SOSP), pages 1\u201317. ACM, 2015.","DOI":"10.1145\/2815400.2815428"},{"key":"13_CR7","unstructured":"C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad apps: End-to-end security via automated full-system verification. In J. Flinn and H. Levy, editors, Operating Systems Design and Implementation (OSDI), pages 165\u2013181. USENIX Association, 2014."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"S. Heule, I. T. Kassios, P. M\u00fcller, and A. J. Summers. Verification condition generation for permission logics with abstract predicates and abstraction functions. In G. Castagna, editor, European Conference on Object-Oriented Programming (ECOOP), volume 7920 of LNCS, pages 451\u2013476. Springer, 2013.","DOI":"10.1007\/978-3-642-39038-8_19"},{"key":"13_CR9","first-page":"315","volume-title":"Lecture Notes in Computer Science","author":"Stefan Heule","year":"2013","unstructured":"S. Heule, K. R. M. Leino, P. M\u00fcller, and A. J. Summers. Abstract read permissions: Fractional permissions without the fractions. In Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 7737 of LNCS, pages 315\u2013334, 2013."},{"key":"13_CR10","unstructured":"J. Kaiser, H. Dang, D. Dreyer, O. Lahav, and V. Vafeiadis. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In P. M\u00fcller, editor, European Conference on Object-Oriented Programming (ECOOP), volume 74 of LIPIcs, pages 17:1\u201317:29. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017."},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"V. Klebanov, P. M\u00fcller, N. Shankar, G. T. Leavens, V. W\u00fcstholz, E. Alkassar, R. Arthan, D. Bronish, R. Chapman, E. Cohen, M. Hillebrand, B. Jacobs, K. R. M. Leino, R. Monahan, F. Piessens, N. Polikarpova, T. Ridge, J. Smans, S. Tobies, T. Tuerk, M. Ulbrich, and B. Weiss. The 1st Verified Software Competition: Experience report. In M. Butler and W. Schulte, editors, Formal Methods (FM), volume 6664 of LNCS, pages 154\u2013168. Springer, 2011.","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. sel4: formal verification of an OS kernel. In J. N. Matthews and T. E. Anderson, editors, Symposium on Operating Systems Principles (SOSP), pages 207\u2013220. ACM, 2009.","DOI":"10.1145\/1629575.1629596"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"K. R. M. Leino and V. W\u00fcstholz. Fine-grained caching of verification results. In Computer Aided Verification (CAV), volume 9206 of LNCS, pages 380\u2013397. Springer, 2015.","DOI":"10.1007\/978-3-319-21690-4_22"},{"key":"13_CR14","unstructured":"P. M\u00fcller. The binomial heap verification challenge in Viper: Online appendix. http:\/\/viper.ethz.ch\/onlineappendix-binomialheap , 2018."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"P. M\u00fcller, M. Schwerhoff, and A. J. Summers. Automatic verification of iterated separating conjunctions using symbolic execution. In S. Chaudhuri and A. Farzan, editors, Computer Aided Verification (CAV), volume 9779 of LNCS, pages 405\u2013425. Springer, 2016.","DOI":"10.1007\/978-3-319-41528-4_22"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"P. M\u00fcller, M. Schwerhoff, and A. J. Summers. Viper: A verification infrastructure for permission-based reasoning. In B. Jobstmann and K. R. M. Leino, editors, Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 9583 of LNCS, pages 41\u201362. Springer, 2016.","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"P. W. O\u2019Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In Computer Science Logic (CSL), pages 1\u201319. Springer, 2001.","DOI":"10.1007\/3-540-44802-0_1"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"M. Parkinson and G. Bierman. Separation logic and abstraction. In J. Palsberg and M. Abadi, editors, Principles of Programming Languages (POPL), pages 247\u2013258. ACM, 2005.","DOI":"10.1145\/1040305.1040326"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"R. Piskac, T. Wies, and D. Zufferey. Automating separation logic with trees and data. In A. Biere and R. Bloem, editors, Computer Aided Verification (CAV), volume 8559 of LNCS, pages 711\u2013728. Springer, 2014.","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"13_CR20","volume-title":"Specification and verification of object-oriented programs","author":"A Poetzsch-Heffter","year":"1997","unstructured":"A. Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, Jan. 1997. https:\/\/softech.cs.uni-kl.de\/homepage\/en\/publications ."},{"key":"13_CR21","unstructured":"M. Schwerhoff and A. J. Summers. Lightweight support for magic wands in an automatic verifier. In J. T. Boyland, editor, European Conference on Object-Oriented Programming (ECOOP), volume 37 of LIPIcs, pages 614\u2013638. Schloss Dagstuhl, 2015."},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"J. Smans, B. Jacobs, and F. Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In European Conference on Object-Oriented Programming (ECOOP), volume 5653 of LNCS, pages 148\u2013172. Springer, 2009.","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"A. J. Summers and S. Drossopoulou. A formal semantics for isorecursive and equirecursive state abstractions. In G. Castagna, editor, European Conference on Object-Oriented Programming (ECOOP), volume 7920 of LNCS, pages 129\u2013153. Springer, 2013.","DOI":"10.1007\/978-3-642-39038-8_6"},{"key":"13_CR24","unstructured":"T. Tuerk. Local reasoning about while-loops. In R. Joshi, T. Margaria, P. M\u00fcller, D. Naumann, and H. Yang, editors, VSTTE 2010. Workshop Proceedings, pages 29\u201339. ETH Zurich, 2010."},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"V. Vafeiadis and C. Narayan. Relaxed separation logic: a program logic for C11 concurrency. In A. L. Hosking, P. T. Eugster, and C. V. Lopes, editors, Object Oriented Programming Systems Languages & Applications (OOPSLA), pages 867\u2013884. ACM, 2013.","DOI":"10.1145\/2544173.2509532"}],"container-title":["Principled Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98047-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T13:15:11Z","timestamp":1572182111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98047-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319980461","9783319980478"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98047-8_13","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}