检索结果-内蒙古大学图书馆

A program logic for obstruction-freedom

Frontiers of Computer Science 2024年第6期18卷 85-100页

作者： Zhao-Hui LI Xin-Yu FENG School of Computer Science and Technology University of Science and Technology of ChinaHefei 230026China Department of Computer Science and Technology Nanjing UniversityNanjing 210023China State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China

Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for software transactional memory(STM)and in anonymous and fault-tolerant distributed ***,existing work can only verify obstruction-freedom of specific data structures(e.g.,STM and list-based algorithms).In this paper,to fill this gap,we propose a program logic that can formally verify obstruction-freedom of practical implementations,as well as verify linearizability,a safety property,at the same *** also propose informal principles to extend a logic for verifying linearizability to verifying *** this approach,the existing proof for linearizability can be reused directly to construct the proof for both linearizability and ***,we have successfully applied our logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.

关键词： verification program logic progress properties obstruction-freedom concurrent objects

来源：评论

学校读者我要写书评

暂无评论

Goal-Aware RSS for Complex Scenarios via program logic

IEEE TRANSACTIONS ON INTELLIGENT VEHICLES

引用

IEEE TRANSACTIONS ON INTELLIGENT VEHICLES 2023年第4期8卷 3040-3072页

作者： Hasuo, Ichiro Eberhart, Clovis Haydon, James Dubut, Jeremy Bohrer, Rose Kobayashi, Tsutomu Pruekprasert, Sasinee Zhang, Xiao-Yi Pallas, Erik Andre Yamada, Akihisa Suenaga, Kohei Ishikawa, Fuyuki Kamijo, Kenji Shinya, Yoshiyuki Suetomi, Takamasa Natl Inst Informat Tokyo 1018430 Japan SOKENDAI Grad Univ Adv Studies Hayama 1018430 Japan Japanese French Lab Informat IRL 3527 Tokyo 1350064 Japan Worcester Polytech Inst Dept Comp Sci Worcester MA 01609 USA Kyoto Univ Grad Sch Informat Kyoto 6068501 Japan Mazda Motor Corp Fuchu 7308670 Japan

We introduce a goal-aware extension of responsibility sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement-in addition to collision avoidance as in the original RSS-requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reasoning framework based on program logic, in which one can systematically develop RSS rules for smaller subscenarios and combine them to obtain RSS rules for bigger scenarios. As the basis of the framework, we introduce a program logic dFHL that accommodates continuous dynamics and safety conditions. Our framework presents a dFHL-based workflow for deriving goal-aware RSS rules;we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goal-aware RSS is indeed effective in realising both collision avoidance and goal achievement.

关键词： Safety Automobiles Collision avoidance Intelligent vehicles Cognition Planning Computer architecture Automated driving differential dynamics Floyd-Hoare logic program logic responsibility-sensitive safety (RSS) rule-based safety safety simplex architecture

来源：评论

学校读者我要写书评

暂无评论

Goal-Aware RSS for Complex Scenarios via program logic 35

Goal-Aware RSS for Complex Scenarios via Program Logic

引用

IEEE Intelligent Vehicles Symposium (IV)

作者： Hasuo, Ichiro Eberhart, Clovis Haydon, James Dubut, Jeremy Bohrer, Rose Kobayashi, Tsutomu Pruekprasert, Sasinee Zhang, Xiao-Yi Pallas, Erik Andre Yamada, Akihisa Suenaga, Kohei Ishikawa, Fuyuki Kamijo, Kenji Shinya, Yoshiyuki Suetomi, Takamasa Natl Inst Informat NII Tokyo 1018430 Japan Worcester Polytech Inst Dept Comp Sci 100 Inst Rd Worcester MA 01609 USA Univ Augsburg Inst Software & Syst Engn Univ Str 6a D-86135 Augsburg Germany AIST Cyber Phys Secur Res Ctr Aomi 2-4-7 Tokyo 1350064 Japan Kyoto Univ Grad Sch Informat Kyoto 6068501 Japan Mazda Motor Corp Fuchu Tokyo 7308670 Japan SOKENDAI Hayama Kanagawa Japan Japanese French Lab Informat IRL 3527 Tokyo Japan NII Tokyo Japan

ISBN: (纸本)9798350348811;9798350348828

We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement-in addition to collision avoidance as in the original RSS-requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reasoning framework based on program logic, in which one can systematically develop RSS rules for smaller subscenarios and combine them to obtain RSS rules for bigger scenarios. As the basis of the framework, we introduce a program logic dFHL that accommodates continuous dynamics and safety conditions. Our framework presents a dFHL-based workflow for deriving goal-aware RSS rules;we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goal-aware RSS is indeed effective in realising both collision avoidance and goal achievement.

关键词： automated driving safety rule-based safety responsibility-sensitive safety (RSS) program logic Floyd-Hoare logic differential dynamics simplex architecture

来源：评论

学校读者我要写书评

暂无评论

program logic for Higher-Order Probabilistic programs in Isabelle/HOL 1

引用

16th International Symposium on Functional and logic programming (FLOPS)

作者： Hirata, Michikazu Minamide, Yasuhiko Sato, Tetsuya Tokyo Inst Technol Sch Comp Tokyo Japan

ISBN: (数字)9783030994617

ISBN: (纸本)9783030994600;9783030994617

The verification framework PPV (Probabilistic program Verification) verifies functional probabilistic programs supporting higher-order functions, continuous distributions, and conditional inference. PPV is based on the theory of quasi-Borel spaces which is introduced to give a semantics of higher-order probabilistic programming languages with continuous distributions. In this paper, we formalize a theory of quasi-Borel spaces and a core part of PPV in Isabelle/HOL. We first construct a probability monad on quasi-Borel spaces based on the Giry monad in the Isabelle/HOL library. Our formalization of PPV is extended so that integrability of functions can be discussed formally. Finally, we prove integrability and convergence of the Monte Carlo approximation in our mechanized PPV.

关键词： Higher-order probabilistic programming language program logic Formal verification Isabelle/HOL

来源：评论

学校读者我要写书评

暂无评论

program logic for higher-order probabilistic programs in Isabelle/HOL

引用

SCIENCE OF COMPUTER programMING 2023年第1期230卷

作者： Hirata, Michikazu Minamide, Yasuhiko Sato, Tetsuya Tokyo Inst Technol Sch Comp Meguro ku 2-12-1 Tokyo 1528550 Japan

关键词： Higher-order probabilistic programming language program logic Formal verification Quasi -Borel spaces Isabelle HOL

来源：评论

学校读者我要写书评

暂无评论

A Correctness and Incorrectness program logic

引用

JOURNAL OF THE ACM 2023年第2期70卷 15-15页

作者： Bruni, Roberto Giacobazzi, Roberto Gori, Roberta Ranzato, Francesco Univ Pisa Pisa Italy Univ Verona Verona Italy Univ Padua Padua Italy

interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. Completeness means that the abstract interpreter reports no false alarms for all possible inputs, but this is extremely rare because it needs a very precise analysis. We introduce a weaker notion of completeness, called local completeness, which requires that no false alarms are produced only relatively to some fixed program inputs. Based on this idea, we introduce a program logic, called Local Completeness logic for an abstract domain A, for proving both the correctness and incorrectness of program specifications. Our proof system, which is parameterized by an abstract domain A, combines over- and under-approximating reasoning. In a provable triple proves(A) [p] c [q], c is a program, q is an under-approximation of the strongest post-condition of c on input p such that their abstractions in A coincide. This means that q is never too coarse, namely, under some mild assumptions, the abstract interpretation of c does not yield false alarms for the input p iff q has no alarm. Therefore, proving proves(A) [p] c [q] not only ensures that all the alarms raised in q are true ones, but also that if q does not raise alarms, then c is correct. We also prove that if A is the straightforward abstraction making all program properties equivalent, then our program logic coincides with O'Hearn's incorrectness logic, while for any other abstraction, contrary to the case of incorrectness logic, our logic can also establish program correctness.

关键词： Abstract interpretation abstract domain program analysis program verification program logic local completeness best correct approximation incorrectness logic

来源：评论

学校读者我要写书评

暂无评论

program logic of a mental health outreach service for socially anxious youth

引用

EVALUATION AND program PLANNING 2023年 97卷 102250页

作者： Benstead, M. L. Stones, J. Gibson, G. Moody, L. J. Little, K. Toumbourou, J. W. Deakin Univ Ctr Social & Early Emot Dev Sch Psychol 1 Gheringhap St Geelong 3220 Australia Headspace Geelong 105 Yarra St Geelong 3220 Australia Barwon Child Youth & Family 222 Malop St Geelong 3220 Australia Deakin Univ Sch Med Waurn Ponds 3216 Australia Deakin Univ Sch Psychol 221 Burwood Hwy Burwood Vic 3125 Australia

Youth mental health is a major concern both in Australia and internationally. Identifying at-risk young people is a core service priority. This report describes a "Youth Social Inclusion program" developed in Australia to assist young people identified as having social difficulties that prevent them linking into formal mental health services. This report describes the Australian service context and uses the "program explication" methodology to document: the program activities, therapeutic processes, and underpinning evidence for the benefits of this service. program explication is a consulting method designed to assist services to identify and review implicit program logic assumptions against evaluation literature. We demonstrate the application of this method in exploring the assumptions and evidence for the Youth Social Inclusion program, targeting outreach to socially anxious young people in Australia. The Youth Social Inclusion program involved seven logically consistent activities. Our literature search revealed moderate evidence for the expected benefits of the activities. This practice-based design drew on several theoretical perspectives. Given that the program logic has been established, we outline a proposal for further evaluation.

关键词： Youth Mental health Outreach Social anxiety program logic

来源：评论

学校读者我要写书评

暂无评论

A program logic for fresh name generation

引用

SCIENCE OF COMPUTER programMING 2022年 223卷

作者： Eliott, Harold Pancho Berger, Martin Univ Sussex Dept Informat Brighton E Sussex England Huawei 2012 Labs Turing Core London England

We present a program logic for Pitts and Stark???s v-calculus, an extension of the call-byvalue simply-typed A-calculus with a mechanism for the generation of fresh names. Names can be compared for equality and inequality, producing programs with subtle observable properties. Hidden names produced by interactions between generation and abstraction are captured logically with a second-order quantifier over type contexts. We illustrate usage of the logic through reasoning about well-known difficult cases from the literature. ?? 2022 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY-NC-ND license (http://***/licenses/by-nc-nd/4.0/).

关键词： programming language Lambda -calculus Fresh name generation program logic program verification

来源：评论

学校读者我要写书评

暂无评论

Persistent Owicki-Gries Reasoning A program logic for Reasoning about Persistent programs on Intel-x86

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2020年第OOPSLA期4卷 1–28页

作者： Raad, Azalea Lahav, Ori Vafeiadis, Viktor MPI SWS Saarland Informat Campus Saarbrucken Germany Imperial Coll London South Kensington Campus London England Tel Aviv Univ Sch Comp Sci IL-69978 Tel Aviv Israel

The advent of non-volatile memory (NVM) technologies is expected to transform how software systems are structured fundamentally, making the task of correct programming significantly harder. This is because ensuring that memory stores persist in the correct order is challenging, and requires low-level programming to flush the cache at appropriate points. This has in turn resulted in a noticeable verification gap. To address this, we study the verification of NVM programs, and present Persistent Owicki-Gries (POG), the first program logic for reasoning about such programs. We prove the soundness of POG over the recent Intel-x86 model, which formalises the out-of-order persistence of memory stores and the semantics of the Intel cache line flush instructions. We then use POG to verify several programs that interact with NVM.

关键词： non-volatile memory program logic x86-ISO consistency persistency

来源：评论

学校读者我要写书评

暂无评论

A program logic for Reasoning About C11 programs With Release-Sequences

引用

IEEE ACCESS 2020年 8卷 173874-173903页

作者： He, Mengda Qin, Shengchao Xu, Zhiwu Teesside Univ Sch Comp Engn & Digital Technol Middlesbrough TS1 3BX Cleveland England Shenzhen Univ Coll Comp Sci & Software Engn Shenzhen 518060 Peoples R China

With the popularity of weak/relaxed memory models widely used in modern hardware architectures, the C11 standard introduced a language level weak memory model, A.K.A the C11 memory model, that allows C/C++ programs to exploit the optimisation provided by the hardware platform in memory ordering and gain benefits in efficiency. On the other hand, with the weakened memory ordering allowed, more program behaviours are introduced, among which some are counterintuitive and make it even more challenging for programmers to understand or to formally reason about C11 multithread programs. To support the formal verification of the C11 weak memory programs, several program logics, e.g. RSL, GPS, FSL, and GPS+, have been developed during the last few years. However, due to the complexity of the weakened memory model, some intricate C11 features still cannot be handled in these logics. A notable example is the lack of supporting to the reasoning about a highly flexible C11 synchronisation mechanism, the release-sequence. Recently, the FSL++ logic proposed by Doko and Vafeiadis moves one step forward to address this problem, but FSL++ only considers the scenarios with atomic update operations in a release-sequence. In this article, we propose a new program logic, GPS++, that supports the reasoning about C11 programs with fully featured release-sequences. We also introduce fractional read permissions to GPS++, which are essential to the reasoning about a large number of real-world concurrent programs. GPS++ is a successor of our previous program logic GPS+, but it comes with much finer control over the resource transmission with the newly introduced restricted-shareable assertions and an enhanced protocol system. A more sophisticated resource model is devised to support the soundness proof of our new program logic. We also demonstrate GPS++ in action by verifying C11 programs with release-sequences that could not be handled by existing program logics.

关键词： Cognition Synchronization Hardware Global Positioning System Instruction sets Load modeling Radio frequency program logic formal semantics program verification C11 weak memory model release-sequence

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：