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

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

An observationally complete program logic for imperative higher-order functions

引用

THEORETICAL COMPUTER SCIENCE 2014年 517卷 75-101页

作者： Honda, Kohei Yoshida, Nobuko Berger, Martin Univ London Dept Comp Sci London WC1E 7HU England Univ London Imperial Coll Sci Technol & Med Dept Comp London SW7 2AZ England Univ Sussex Dept Informat Brighton BN1 9RH E Sussex England

We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state. (C) 2013 Elsevier B.V. All rights reserved.

关键词： Completeness Characteristic formulae program logic Higher-order function Imperative programming Observational equivalence

来源：评论

学校读者我要写书评

暂无评论

Comparing some intuitions of 'process calculus' and 'program logic'

引用

JOURNAL OF logic AND COMPUTATION 2001年第6期11卷 789-827页

作者： Steel, S Univ Essex Dept Comp Sci Colchester CO4 3SQ Essex England

Suppose one needs to reason about about evolving systems such as programs or agents. One standard tradition (die 'event-and-order tradition') describes what the system does as a tree of possible events, with forks as choices or discoveries. Process calculus is a typical version. Another tradition (the 'state-and-Lime tradition') describes what the system does as a set of alternative histories (sequences of states) that the system can drive the world through as it acts. Dynamic and temporal logics are typical versions. One contribution of this paper is an account of how a process seen as a tree in the event-and-order tradition can be understood as an abstraction of a process seen as a set of alternative histories in the state-and-time tradition. The abstraction can be formalized as two equivalence relations, one between states on a single history, which describe the edges in the process seen as a tree, and one between states on different histories, which describes the forking in the process seen as a tree. It is shown that, exactly what such an abstraction omits is information about which points in two separate processes seen as trees can be reached together. However, the paper arose from the author's difficulty in understanding which tradition was more appropriate for a particular area of artificial intelligence. Because of that, the paper also contrasts some of the intuitions behind the traditions about how to describe the world.

关键词： Action Choice Event Observation Process calculus program logic State

来源：评论

学校读者我要写书评

暂无评论

A program logic for Concurrent Objects under Fair Scheduling

引用

ACM SIGPLAN NOTICES 2016年第1期51卷 385-399页

作者： Liang, Hongjin Feng, Xinyu Univ Sci & Technol China Sch Comp Sci & Technol Beijing Peoples R China Univ Sci & Technol China Suzhou Inst Adv Study Beijing Peoples R China

Existing work on verifying concurrent objects is mostly concerned with safety only, e.g., partial correctness or linearizability. Although there has been recent work verifying lock-freedom of non-blocking objects, much less efforts are focused on deadlock-freedom and starvation-freedom, progress properties of blocking objects. These properties are more challenging to verify than lock-freedom because they allow the progress of one thread to depend on the progress of another, assuming fair scheduling. We propose LiLi, a new rely-guarantee style program logic for verifying linearizability and progress together for concurrent objects under fair scheduling. The rely-guarantee style logic unifies thread modular reasoning about both starvation-freedom and deadlock freedom in one framework. It also establishes progress-aware abstraction for concurrent objects, which can be applied when verifying safety and liveness of client code. We have successfully applied the logic to verify starvation-freedom or deadlock-freedom of representative algorithms such as ticket locks, queue locks, lock-coupling lists, optimistic lists and lazy lists.

关键词： Theory Verification Concurrency Progress program logic Rely-Guarantee Reasoning Refinement

来源：评论

学校读者我要写书评

暂无评论

A program logic for resources

引用

THEORETICAL COMPUTER SCIENCE 2007年第3期389卷 411-445页

作者： Aspinall, David Beringer, Lennart Hofmann, Martin Loidl, Hans-Wolfgang Momigliano, Alberto Univ Edinburgh Sch Informat Lab Fdn Comp Sci Edinburgh EH9 3JZ Midlothian Scotland Univ Munich Inst Informat D-80538 Munich Germany

We introduce a reasoning infrastructure for proving statements about resource consumption in a fragment of the Java Virtual Machine Language (JVML). The infrastructure is based on a small hierarchy of program logics, with increasing levels of abstraction: at the top there is a type system for a high-level language that encodes resource consumption. The infrastructure is designed to be used in a proof-carrying code (PCC) scenario, where mobile programs can be equipped with formal evidence that they have predictable resource behaviour. This article focuses on the core logic in our infrastructure, a VDM-style program logic for partial correctness, which can make statements about resource consumption alongside functional behaviour. We establish some important results for this logic, including soundness and completeness with respect to a resource-aware operational semantics for the JVML. We also present a second logic built on top of the core logic, which is used to express termination;it too is shown to be sound and complete. We then outline how high-level language type systems may be connected to these logics. The entire infrastructure has been formalized in Isabelle/HOL, both to enhance the confidence in our meta-theoretical results, and to provide a prototype implementation for PCC. We give examples to show the usefulness of this approach, including proofs of resource bounds on code resulting from compiling high-level functional programs. (c) 2007 Published by Elsevier B.V.

关键词： program logic proof-carrying-code object-oriented languages Java virtual machine language cost modelling quantitative typesystems lightweight verification

来源：评论

学校读者我要写书评

暂无评论

Using the program logic Model to Evaluate Cuidate!: A Sexual Health program for Latino Adolescents in a School-Based Health Center

引用

WORLDVIEWS ON EVIDENCE-BASED NURSING 2015年第5期12卷 297-305页

作者： Serowoky, Mary L. George, Nancy Yarandi, Hossein Univ Detroit Mercy & Henry Ford Hlth Syst Coll Hlth Profess Detroit MI 48221 USA Wayne State Univ Coll Nursing DNP Program Detroit MI 48202 USA Wayne State Univ Coll Nursing Detroit MI 48202 USA

BackgroundAddressing the disparities in pregnancy and sexually transmitted infection (STI) rates for Latino youth in the United States requires an evidence-based approach. Although randomized controlled trials for sexual risk reduction interventions have shown promise in improving short-term outcomes, program sustainability has not been extensively examined in school settings where teens spend time. Latina teen pregnancy rates are nearly twice the national average. Adolescents comprise only 17% of the U.S. population, yet they account for 50% of STIs. Cuidate! is a high-impact sexual health group program endorsed by the Centers for Disease Control and Prevention that has not been replicated in a real-world setting. AimsThe program logic model (PLM) was used as the systematic approach to plan, implement, and evaluate a sustainable model of sexual health group programing (Cuidate!) in a U.S. high school with a large Latino student population. MethodsThe PLM provided the framework for the evaluation of outputs, outcome, and impact. A multivariate repeated measures analysis of variance was used as the means to evaluate the participant outcomes immediately postprogram and at 8-12 weeks. ResultsCuidate! was executed within an existing school structure and time constraints, below cost projections, and with high participant retention (95.8%). Three cohorts (N = 24) of female teens demonstrated significant increases in STI or HIV knowledge, self-efficacy, and intention to use condoms (p < .01). Condom use increased postprogram. No participants initiated sexual behavior, nor were there any reported pregnancies or STIs. ConclusionsAn evidence-based intervention previously tested in randomized controlled trials can be sustained in a school-based health center with similar results of efficacy. Linking Evidence to ActionOur success served as a platform for a sustainable program. We continue to extend the impact of the program by delivering Cuidate! in the school setting using a c

关键词： adolescent sexual health adolescent sexual risk reduction Cuidate pregnancy prevention in Latino teens pregnancy and STI or HIV prevention in schools program evaluation program logic school-based health center STI or HIV prevention in Latino teens

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：