{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T16:22:23Z","timestamp":1792254143610,"version":"4.4.0"},"reference-count":75,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,7]]},"DOI":"10.1109\/hpcsim.2012.6266896","type":"proceedings-article","created":{"date-parts":[[2012,8,22]],"date-time":"2012-08-22T14:48:48Z","timestamp":1345646928000},"page":"91-97","source":"Crossref","is-referenced-by-count":5,"title":["Towards verified cloud computing environments"],"prefix":"10.1109","author":[{"given":"Frederic","family":"Loulergue","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frederic","family":"Gava","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthieu","family":"Lemerre","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"35","first-page":"257","article-title":"Parallel Programming and Performance Predictability with Orle?ans Skeleton Library","author":"javed","year":"2011","journal-title":"High Performance Computing and Simulation Conference (HPCS'07)"},{"key":"36","author":"tesson","year":"2011","journal-title":"Environnement Pour Le De?veloppement et la Preuve de Correction Syste?matiques de Programmes Paralle?les Fonctionnels"},{"key":"33","author":"o'sullivan","year":"2008","journal-title":"Real World Haskell"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1145\/1146847.1146860"},{"key":"39","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2009.05.021"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1109\/PDCAT.2010.86"},{"key":"38","first-page":"1046","article-title":"Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction","volume":"3515","author":"loulergue","year":"2005","journal-title":"LNCS"},{"key":"43","article-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","volume":"2283","author":"nipkow","year":"2002","journal-title":"LNCS"},{"key":"42","first-page":"254","article-title":"Generate, Test, and Aggregate - A Calculation-based Framework for Systematic Parallel Programming with MapReduce","volume":"7211","author":"emoto","year":"2012","journal-title":"LNCS"},{"key":"41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23397-5_5"},{"key":"40","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.07.001"},{"key":"67","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"66","doi-asserted-by":"publisher","DOI":"10.1145\/361011.361067"},{"key":"69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_5"},{"key":"68","year":"0","journal-title":"Common Criteria Recognition Arrangement"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"key":"23","first-page":"165","article-title":"A survey and classification of some program transformation approaches and techniques","author":"feather","year":"1987","journal-title":"Program Specification and Transformation Proc IFIP TC2\/WG 2 1 Working Conf"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-87374-4_1"},{"key":"25","author":"jeuring","year":"1993","journal-title":"Theories for Algorithm Calculation"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61455-2_12"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1142\/S0129626495000175"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268972"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480905"},{"key":"3","first-page":"83","article-title":"Verifying two lines of C with Why3: An exercise in program verification","volume":"7152","author":"fillia?tre","year":"2012","journal-title":"LNCS"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926387"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-74884-4_5"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813672"},{"key":"4","year":"0","journal-title":"The Coq Proof Assistant"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006058"},{"key":"70","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-3-642-15057-9_3","article-title":"Automated verification of a small hypervisor","author":"alkassar","year":"2010","journal-title":"Proc Verified Software Theories Tools Experiments (VSTTE'05)"},{"key":"71","first-page":"23","article-title":"VCC: A practical system for verifying concurrent C","volume":"5674","author":"cohen","year":"2009","journal-title":"LNCS"},{"key":"9","author":"chailloux","year":"2000","journal-title":"De?veloppement d'Applications Avec Objective Caml"},{"key":"72","author":"baudin","year":"2011","journal-title":"ACSL ANSI\/ISO C Specification Language"},{"key":"8","author":"leroy","year":"2010","journal-title":"The Objective Caml System Release 3 11"},{"key":"73","author":"correnson","year":"2011","journal-title":"Frama-C User Manual"},{"key":"74","author":"wiedijk","year":"0","journal-title":"Estimating the Cost of A Standard Library for A Mathematical Proof Checker"},{"key":"75","doi-asserted-by":"publisher","DOI":"10.1145\/1863482.1863491"},{"key":"59","author":"gosling","year":"2011","journal-title":"The Java Language Specification"},{"key":"58","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"57","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"56","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/79173.79181"},{"key":"55","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"17","author":"pelagatti","year":"1998","journal-title":"Structured Development of Parallel Programs"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1026"},{"key":"15","year":"2012","journal-title":"Oracle JRockit Virtual Edition"},{"key":"16","author":"cole","year":"1989","journal-title":"Algorithmic Skeletons Structured Management of Parallel Computation"},{"key":"13","author":"lindholm","year":"2011","journal-title":"The Java Virtual Machine Specification"},{"key":"14","author":"odersky","year":"2010","journal-title":"Programming in Scala"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/1807167.1807184"},{"key":"12","author":"white","year":"2010","journal-title":"Hadoop The Definitive Guide"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198529392.001.0001"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/CloudCom.2010.17"},{"key":"64","doi-asserted-by":"publisher","DOI":"10.1109\/ISORCW.2011.15"},{"key":"65","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224076"},{"key":"62","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706313"},{"key":"63","doi-asserted-by":"publisher","DOI":"10.1145\/1519130.1519131"},{"key":"60","author":"altherr","year":"2006","journal-title":"A Typed Intermediate Language and Algorithms for Compiling Scala by Successive Rewritings"},{"key":"61","doi-asserted-by":"publisher","DOI":"10.1145\/1377492.1377499"},{"key":"49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_2"},{"key":"48","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.080"},{"key":"45","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"44","author":"imai","year":"2012","journal-title":"Coq2Scala"},{"key":"47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"46","first-page":"364","article-title":"Boogie: A Modular Reusable Verifier for Object-Oriented Programs","author":"barnett","year":"2005","journal-title":"Symp on Formal Methods for Components and Objects (FMCO)"},{"key":"10","first-page":"137","article-title":"MapReduce: Simplified Data Processing on Large Clusters","author":"dean","year":"2004","journal-title":"6th Symposium on Operating Systems Design and Implementation (OSDI'04)"},{"key":"51","doi-asserted-by":"publisher","DOI":"10.1142\/S0129626403001343"},{"key":"52","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2011.04.005"},{"key":"53","author":"stolpmann","year":"2011","journal-title":"The Plasma Project"},{"key":"54","first-page":"13","article-title":"Permission-Based Separation Logic for Multithreaded Java Programs","volume":"15","author":"haack","year":"2011","journal-title":"Nieuwsbrief Van de Nederlandse Vereniging Voor Theoretische Informatica"},{"key":"50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_24"}],"event":{"name":"2012 International Conference on High Performance Computing & Simulation (HPCS)","location":"Madrid, Spain","start":{"date-parts":[[2012,7,2]]},"end":{"date-parts":[[2012,7,6]]}},"container-title":["2012 International Conference on High Performance Computing & Simulation (HPCS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6260982\/6266874\/06266896.pdf?arnumber=6266896","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T23:09:19Z","timestamp":1498000159000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6266896\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":75,"URL":"https:\/\/doi.org\/10.1109\/hpcsim.2012.6266896","relation":{},"subject":[],"published":{"date-parts":[[2012,7]]}}}