{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T21:10:28Z","timestamp":1743628228322,"version":"3.40.3"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","license":[{"start":{"date-parts":[[2012,7,1]],"date-time":"2012-07-01T00:00:00Z","timestamp":1341100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2012,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Stepwise refinement is a well-studied technique for developing a program from an abstract description to a concrete implementation. This paper describes a system with automated tool support for refinement, powered by a state-of-the-art verification engine that uses an SMT solver. Unlike previous refinement systems, users of the presented system interact only via declarations in the programming language. Another aspect of the system is that it accounts for dynamically allocated objects in the heap, so that data representations in an abstract program can be refined into ones that use more objects. Finally, the system uses a language with familiar imperative features, including sequential composition, loops, and recursive calls, offers a syntax with skeletons for describing program changes between refinements, and provides a mechanism for supplying witnesses when refining non-deterministic programs.<\/jats:p>","DOI":"10.1007\/s00165-012-0254-3","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T08:35:50Z","timestamp":1340872550000},"page":"519-535","source":"Crossref","is-referenced-by-count":4,"title":["Stepwise refinement of heap-manipulating code in Chalice"],"prefix":"10.1145","volume":"24","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[{"name":"Microsoft Research, One Microsoft Way, 98052, Redmond, WA, USA"}]},{"given":"Kuat","family":"Yessenov","sequence":"additional","affiliation":[{"name":"MIT Computer Science and Artificial Intelligence Lab, Cambridge, MA, USA"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Butler M Hallerstede S Hoang TS Mehta F Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transf","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2003) Event based sequential program development: Application to constructing a pointer program. In: Araki K Gnesi S Mandrioli D (eds) FME 2003: formal methods international symposium of formal methods Europe. Lecture Notes in Computer Science vol 2805. Springer Berlin pp 51\u201374","DOI":"10.1007\/978-3-540-45236-2_5"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2006) Formal methods in industry: achievements problems future. In: Osterweil LJ Dieter Rombach H Soffa ML (eds) 28th international conference on software engineering (ICSE 2006). ACM New York pp 761\u2013768","DOI":"10.1145\/1134285.1134406"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_7_2","unstructured":"Back RJR (1978) On the correctness of refinement steps in program development. PhD thesis University of Helsinki. Report A-1978-4."},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Barnett M Chang B-YE DeLine R Jacobs B Leino KRM (2006) Boogie: a modular reusable verifier for object-oriented programs. In: de Boer FS Bonsangue MM Graf S de Roever W-P (eds) Formal methods for components and objects: 4th international symposium FMCO 2005. Lecture Notes in Computer Science vol. 4111. Springer Berlin pp 364\u2013387","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_2_1_2_11_2","unstructured":"Baudin P Filli\u00e2tre JC March\u00e9 C Monate B Moy Y Prevosto V (2009) ACSL: ANSI\/ISO C specification language version 1.4. http:\/\/frama-c.com\/"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Ball T Hackett B Lahiri SK Qadeer S Vanegue J (2010) Towards scalable modular checking of user-defined properties. In: Leavens GT O\u2019Hearn P Rajamani SK (eds) Verified software: theories tools experiments (VSTTE 2010). Lecture Notes in Computer Science vol 6217. Springer Berlin pp 1\u201324","DOI":"10.1007\/978-3-642-15057-9_1"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650070034"},{"key":"#cr-split#-e_1_2_1_2_14_2.1","doi-asserted-by":"crossref","unstructured":"Boyland J (2003) Checking interference with fractional permissions. In: Cousot R","DOI":"10.1007\/3-540-44898-5_4"},{"key":"#cr-split#-e_1_2_1_2_14_2.2","unstructured":"(ed) Static analysis 10th international symposium SAS 2003. Lecture Notes in Computer Science vol 2694. Springer Berlin pp 55-72"},{"issue":"1","key":"e_1_2_1_2_15_2","first-page":"17","article-title":"Stepwise refinement of action systems","volume":"12","author":"Back R-J","year":"1991","journal-title":"Struct Program"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/551462"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Clarke D Drossopoulou S (2002) Ownership encapsulation and the disjointness of type and effect. In: Proceedings of the 2002 ACM SIGPLAN conference on object-oriented programming systems languages and applications OOPSLA 2002. ACM New York pp 292\u2013310","DOI":"10.1145\/583854.582447"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Cohen E Dahlweid M Hillebrand M Leinenbach D Moskal M Santen T Schulte W Tobies S (2009) VCC: a practical system for verifying concurrent C. In: Berghofer S Nipkow T Urban C Wenzel M (eds) Theorem proving in higher order logics 22nd international conference TPHOLs 2009. Lecture Notes in Computer Science vol 5674. Springer Berlin pp 23\u201342","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_2_19_2","unstructured":"ClearSy. Atelier B. http:\/\/www.atelierb.eu\/."},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Carter G Monahan R Morris JM (2005) Software refinement with perfect developer. In: Aichernig BK Beckert B (eds) Third IEEE international conference on software engineering and formal methods (SEFM 2005). IEEE Computer Society New York pp 363\u2013373","DOI":"10.1109\/SEFM.2005.41"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01933419"},{"volume-title":"A discipline of programming","year":"1976","author":"Dijkstra EW","key":"e_1_2_1_2_23_2"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"de Moura L Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS 2008. Lecture Notes in Computer Science vol 4963. Springer Berlin pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_25_2","unstructured":"Dahl O-J Myhrhaug B Nygaard K (1970) Common base language. Publication S-22 Norwegian Computing Center"},{"key":"e_1_2_1_2_26_2","unstructured":"Escher Technologies Inc. (2001) Getting started with perfect. http:\/\/www.eschertech.com"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0125-8"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Gries D Prins J (1985) A new notion of encapsulation. In: Proceedings of the ACM SIGPLAN 85 symposium on language issues in programming environments. SIGPLAN Notices vol 20 No. 7. ACM New York pp 131\u2013139","DOI":"10.1145\/17919.806834"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Grandy H Stenzel K Reif W (2007) A refinement method for Java programs. In: Bonsangue MM Johnsen EM (eds) Formal methods for open object-based distributed systems 9th IFIP WG 6.1 international conference FMOODS 2007. Lecture Notes in Computer Science vol 4468. Springer Berlin pp 221\u2013235","DOI":"10.1007\/978-3-540-72952-5_14"},{"issue":"1","key":"e_1_2_1_2_30_2","first-page":"1","article-title":"The transform\u2014a new language construct","volume":"11","author":"Gries D","year":"1990","journal-title":"Struct Program"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Heule S Kassios IT M\u00fcller P Summers AJ (2012) Verification condition generation for permission logics with abstraction functions. Technical Report 761 ETH Zurich","DOI":"10.1007\/978-3-642-39038-8_19"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Hatcliff J Leavens GT Rustan M. Leino K M\u00fcller P Parkinson M (2012) Behavioral interface specification languages. ACM Comput Surv 44(3)","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Heule S Rustan M. Leino K M\u00fcller P Summers AJ (2011) Fractional permissions without the fractions. In: 13th workshop on formal techniques for Java-like programs FTfJP 2011","DOI":"10.1145\/2076674.2076675"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"volume-title":"Software abstractions: logic, language, and analysis","year":"2006","author":"Jackson D","key":"e_1_2_1_2_35_2"},{"key":"e_1_2_1_2_36_2","unstructured":"Jones CB (1990) Systematic software development using VDM. International Series in Computer Science 2nd edn. Prentice Hall Englewood Cliffs"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00122417"},{"key":"e_1_2_1_2_38_2","unstructured":"Jacobs B Piessens F (2006) The VeriFast program verifier. Technical Report CW-520 Department of Computer Science Katholieke Universiteit Leuven"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Kassios IT (2006) Dynamic frames: support for framing dependencies and sharing without restrictions. In: Misra J Nipkow T Sekerinski E (eds) FM 2006: formal methods 14th international symposium on formal methods. Lecture Notes in Computer Science vol 4085. Springer Berlin pp 268\u2013283","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Klein G Sewell T Winwood S (2010) Refinement in the formal verification of seL4. In: Hardin DS (ed) Design and verification of microprocessor systems for high-assurance applications. Springer Berlin pp 323\u2013339","DOI":"10.1007\/978-1-4419-1539-9_11"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Butler M (2003) ProB: a model checker for B. In: Araki K Gnesi S Mandrioli D (eds) FME 2003: formal methods. Lecture Notes in Computer Science vol 2805. Springer Berlin pp 855\u2013874","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.300040"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Clarke EM Voronkov A (eds) LPAR-16. Lecture Notes in Computer Science vol 6355. Springer Berlin pp 348\u2013370","DOI":"10.1007\/978-3-642-17511-4_20"},{"volume-title":"Abstraction and specification in program development. MIT Electrical Engineering and Computer Science Series","year":"1986","author":"Liskov B","key":"e_1_2_1_2_44_2"},{"key":"#cr-split#-e_1_2_1_2_45_2.1","doi-asserted-by":"crossref","unstructured":"Leino KRM M\u00fcller P (2006) A verification methodology for model fields. In: Sestoft P","DOI":"10.1007\/11693024_9"},{"key":"#cr-split#-e_1_2_1_2_45_2.2","unstructured":"(ed) Programming languages and systems 15th European symposium on programming ESOP 2006. Lecture Notes in Computer Science vol 3924. Springer Berlin pp 115-130"},{"key":"#cr-split#-e_1_2_1_2_46_2.1","doi-asserted-by":"crossref","unstructured":"Leino KRM M\u00fcller P (2009) A basis for verifying multi-threaded programs. In: Castagna G","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"#cr-split#-e_1_2_1_2_46_2.2","unstructured":"(ed) Programming languages and systems 18th European Symposium on Programming ESOP 2009. Lecture Notes in Computer Science vol 5502. Springer Berlin pp 378-393"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Leino KRM M\u00fcller P Smans J (2009) Verification of concurrent programs with Chalice. In: Aldini A Barthe G Gorrieri R (eds) Foundations of security analysis and design V: FOSAD 2007\/2008\/2009 tutorial lectures. Lecture Notes in Computer Science vol 5705. Springer Berlin pp 195\u2013222","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Leino KRM R\u00fcmmer P (2010) A polymorphic intermediate verification language: design and logical encoding. In: Esparza J Majumdar R (eds) Tools and algorithms for the construction and analysis of systems 16th international conference TACAS 2010. Lecture Notes in Computer Science vol 6015. Springer Berlin pp 312\u2013327","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Liskov B Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6)","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_2_51_2","unstructured":"Meyer B (1998) Object-oriented software construction. Series in Computer Science. Prentice-Hall NJ"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Martin AJ Lines A Manohar R Nystr\u00f6m M P\u00e9nzes PI Southworth R Cummings U (1997) The design of an asynchronous MIPS R3000 microprocessor. In: 17th conference on advanced research in VLSI ARVLSI \u201997. IEEE Computer Society New York pp 164\u2013181","DOI":"10.1109\/ARVLSI.1997.634853"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_2_54_2","unstructured":"Morgan C (1990) Programming from specifications. Series in Computer Science. Prentice-Hall International NJ"},{"key":"e_1_2_1_2_55_2","unstructured":"Morgan C (1994) The cuppest capjunctive capping and Galois. In: Roscoe AW (ed) A classical mind: essays in honour of C.A.R. Hoare. International Series in Computer Science. Prentice-Hall NJ pp 317\u2013332"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0167-y"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Mikhaljova A Sekerinski E (1997) Class refinement and interface refinement in object-oriented programs. In: Fitzgerald JS Jones CB Lucas P (eds) FME \u201997: industrial applications and strengthened foundations of formal methods 4th international symposium of formal methods Europe. Lecture Notes in Computer Science vol 1313. Springer Berlin pp 82\u2013101","DOI":"10.1007\/3-540-63533-5_5"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Parkinson MJ Bierman GM (2005) Separation logic and abstraction. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL 2005. ACM New York pp 247\u2013258","DOI":"10.1145\/1047659.1040326"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: 17th IEEE symposium on logic in computer science (LICS 2002). IEEE Computer Society New York pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Shield J Hayes IJ (2002) Refining object-oriented invariants and dynamic constraints. In: 9th Asia\u2013Pacific software engineering conference (APSEC 2002). IEEE Computer Society New York pp 52\u201361","DOI":"10.1109\/APSEC.2002.1182975"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Smans J Jacobs B Piessens F. Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou S (ed) ECOOP 2009\u2014Object-oriented programming 23rd European conference. Lecture Notes in Computer Science vol 5653. Springer Berlin pp 148\u2013172","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Tafat A Boulm\u00e9 S March\u00e9 C (2010) A refinement methodology for object-oriented programs. In: Beckert B March\u00e9 C (eds) Formal verification of object-oriented software papers presented at the international conference pp 143\u2013159","DOI":"10.1007\/978-3-642-18070-5_11"},{"key":"e_1_2_1_2_63_2","unstructured":"Woodcock J Davies J (1996) Using Z: Specification refinement and proof. Prentice Hall NJ"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/362575.362577"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0254-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0254-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0254-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T20:56:28Z","timestamp":1743627388000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0254-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":67,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["10.1007\/s00165-012-0254-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0254-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}