{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:26:09Z","timestamp":1729643169053,"version":"3.28.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":3,"title":["Towards verified cloud computing environments"],"prefix":"10.1109","author":[{"given":"Frederic","family":"Loulergue","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frederic","family":"Gava","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthieu","family":"Lemerre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"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)"},{"journal-title":"Environnement Pour Le De?veloppement et la Preuve de Correction Syste?matiques de Programmes Paralle?les Fonctionnels","year":"2011","author":"tesson","key":"36"},{"journal-title":"Real World Haskell","year":"2008","author":"o'sullivan","key":"33"},{"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"},{"journal-title":"Common Criteria Recognition Arrangement","year":"0","key":"68"},{"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"},{"journal-title":"Theories for Algorithm Calculation","year":"1993","author":"jeuring","key":"25"},{"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"},{"journal-title":"The Coq Proof Assistant","year":"0","key":"4"},{"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"},{"journal-title":"De?veloppement d'Applications Avec Objective Caml","year":"2000","author":"chailloux","key":"9"},{"journal-title":"ACSL ANSI\/ISO C Specification Language","year":"2011","author":"baudin","key":"72"},{"journal-title":"The Objective Caml System Release 3 11","year":"2010","author":"leroy","key":"8"},{"journal-title":"Frama-C User Manual","year":"2011","author":"correnson","key":"73"},{"journal-title":"Estimating the Cost of A Standard Library for A Mathematical Proof Checker","year":"0","author":"wiedijk","key":"74"},{"key":"75","doi-asserted-by":"publisher","DOI":"10.1145\/1863482.1863491"},{"journal-title":"The Java Language Specification","year":"2011","author":"gosling","key":"59"},{"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"},{"journal-title":"Structured Development of Parallel Programs","year":"1998","author":"pelagatti","key":"17"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1026"},{"journal-title":"Oracle JRockit Virtual Edition","year":"2012","key":"15"},{"journal-title":"Algorithmic Skeletons Structured Management of Parallel Computation","year":"1989","author":"cole","key":"16"},{"journal-title":"The Java Virtual Machine Specification","year":"2011","author":"lindholm","key":"13"},{"journal-title":"Programming in Scala","year":"2010","author":"odersky","key":"14"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/1807167.1807184"},{"journal-title":"Hadoop The Definitive Guide","year":"2010","author":"white","key":"12"},{"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"},{"journal-title":"A Typed Intermediate Language and Algorithms for Compiling Scala by Successive Rewritings","year":"2006","author":"altherr","key":"60"},{"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"},{"journal-title":"Coq2Scala","year":"2012","author":"imai","key":"44"},{"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"},{"journal-title":"The Plasma Project","year":"2011","author":"stolpmann","key":"53"},{"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)","start":{"date-parts":[[2012,7,2]]},"location":"Madrid, Spain","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]]}}}