乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,13]],"date-time":"2024-06-13T13:55:21Z","timestamp":1718286921881},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"We introduce the abstract domain of correlations to denote equality relations between parts of inputs and outputs of programs. We formalise the theory of correlations, and mechanically verify their semantic properties. We design a static inter-procedural dataflow analysis for automatically inferring correlations for programs written in a first-order language equipped with algebraic data-types and arrays. The analysis, its precision and execution cost, have been evaluated on the code and functional specification of an industrial-size micro-kernel. We exploit the inferred correlations to automatically discharge two thirds of the proof obligations related to the preservation of invariants for this micro-kernel.<\/jats:p>","DOI":"10.1145\/3290360","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Inferring frame conditions with static correlation analysis"],"prefix":"10.1145","volume":"3","author":[{"given":"Oana F.","family":"Andreescu","sequence":"first","affiliation":[{"name":"Internet of Trust, France"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[{"name":"Inria, France \/ Prove & Run, France"}]},{"given":"St\u00e9phane","family":"Lescuyer","sequence":"additional","affiliation":[{"name":"Prove & Run, France"}]},{"given":"Beno\u00eet","family":"Montagu","sequence":"additional","affiliation":[{"name":"Prove & Run, France"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Formal Methods and Software Engineering (LNCS), Michael Butler, Sylvain Conchon, and Fatiha Za\u00efdi (Eds.)","author":"Andreescu Oana"},{"key":"e_1_2_2_2_1","volume-title":"Software Engineering and Formal Methods (LNCS), Rocco De Nicola and Eva K\u00fchn (Eds.)","author":"Andreescu Oana"},{"key":"e_1_2_2_3_1","unstructured":"Oana Fabiana Andreescu. 2017. Static analysis of functional programs with an application to the frame problem in deductive verification. Theses. Universit\u00e9 Rennes 1. https:\/\/tel.archives- ouvertes.fr\/tel- 01677897 Oana Fabiana Andreescu. 2017. Static analysis of functional programs with an application to the frame problem in deductive verification. Theses. Universit\u00e9 Rennes 1. https:\/\/tel.archives- ouvertes.fr\/tel- 01677897"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292535.1292541"},{"key":"e_1_2_2_7_1","volume-title":"Compiler Construction (LNCS)","author":"Cousot Patrick"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349309"},{"key":"e_1_2_2_9_1","volume-title":"The Map Equality Domain. In VSTTE 2018, Proceedings of the 10th Working Conference on Verified Software: Theories, Tools, and Experiments (LNCS)","volume":"11294","author":"Dietsch Daniel","year":"2018"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2893529.2893544"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_26"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69611-7_1"},{"key":"e_1_2_2_14_1","volume-title":"NASA Formal Methods (LNCS)","author":"Illous Hugo"},{"key":"e_1_2_2_15_1","unstructured":"Inria 2017. The Coq proof assistant reference manual. Inria. https:\/\/coq.inria.fr\/distrib\/current\/refman\/ Inria 2017. The Coq proof assistant reference manual. Inria. https:\/\/coq.inria.fr\/distrib\/current\/refman\/"},{"key":"e_1_2_2_16_1","volume-title":"Static Analysis (LNCS)","author":"Jeannet Bertrand"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628159"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/62029.62030"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_2_22_1","unstructured":"Xavier Leroy Damien Doligez Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2017. The Objective Caml system documentation and user\u2019s manual \u2013 release 4.06. INRIA. http:\/\/caml.inria.fr\/pub\/docs\/manual- ocaml- 4.06\/ Xavier Leroy Damien Doligez Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2017. The Objective Caml system documentation and user\u2019s manual \u2013 release 4.06. INRIA. http:\/\/caml.inria.fr\/pub\/docs\/manual- ocaml- 4.06\/"},{"key":"e_1_2_2_23_1","volume-title":"International Workshop on MILS: Architecture and Assurance for Secure Systems.","author":"Lescuyer St\u00e9phane","year":"2015"},{"key":"e_1_2_2_24_1","volume-title":"Compiler Construction (LNCS), G\u00f6rel Hedin (Ed.)","author":"Lhot\u00e1k Ondvrej"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"J. McCarthy and P. J. Hayes. 1981. Some Philosophical Problems from the Standpoint of Artificial Intelligence. In Readings in Artificial Intelligence Bonnie Lynn Webber and Nils J. Nilsson (Eds.). Morgan Kaufmann 431\u2013450. J. McCarthy and P. J. Hayes. 1981. Some Philosophical Problems from the Standpoint of Artificial Intelligence. In Readings in Artificial Intelligence Bonnie Lynn Webber and Nils J. Nilsson (Eds.). Morgan Kaufmann 431\u2013450.","DOI":"10.1016\/B978-0-934613-03-3.50033-7"},{"key":"e_1_2_2_26_1","unstructured":"Bertrand Meyer. 2015. Framing the frame problem. In Dependable Software Systems Engineering. 193\u2013203. Bertrand Meyer. 2015. Framing the frame problem. In Dependable Software Systems Engineering. 193\u2013203."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_2_28_1","volume-title":"Principles of Program Analysis","author":"Nielson Flemming"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_2_32_1","volume-title":"Lam","author":"Whaley John","year":"2002"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290360","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T08:33:06Z","timestamp":1672561986000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290360"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":32,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290360"],"URL":"https:\/\/doi.org\/10.1145\/3290360","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}