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

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

A Correctness and Incorrectness program logic

引用

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

作者： 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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Partners in Recovery: an early phase evaluation of an Australian mental health initiative using program logic and thematic analysis

引用

BMC HEALTH SERVICES RESEARCH 2019年第1期19卷 1-18页

作者： Trankle, Steven A. Reath, Jennifer Western Sydney Univ Dept Gen Practice Sch Med Campbelltown CampusBldg 30-3-18Locked Bag 1797 Penrith NSW 2751 Australia

BackgroundMental illness is a leading cause of illness and disability and around 75% of people suffering mental illness do not have access to adequate care. In Australia, nearly half the population experiences mental illness at some point in their life. The Australian Government developed a National program called Partners in Recovery (PIR) to support those with severe and persistent mental illness. The program was implemented through 48 consortia across Australia. One of these was led by the Nepean Blue Mountains Medicare Local who adapted the program according to its specific local *** conducted an early evaluation of the PIR program in Nepean Blue Mountains (NBMPIR) using a program logic model (PLM) to frame the evaluation and complemented this with an additional thematic analysis. Participants (n=73) included clients and carers, program management and staff of the Consortium and other partners and agencies, and clinical, allied health, and other service providers. Our PLM utilised multiple data sources that included document review, open and closed survey questions, and semi-structured interviews. Quantitative data received a descriptive analysis and qualitative data was analysed both in alignment with the PLM framework and *** aligned our results to PLM domains of inputs, activities, outputs, outcomes and impacts. The NBMPIR consortium implemented a recovery approach and provided greater access to services by enhancing healthcare provider partnerships. Our thematic analysis further described five key themes of collaboration;communication;functioning of PIR;structural/organisational challenges;and understanding of PIR approaches. Facilitators and barriers to the NBMPIR program centred on the alignment of vision and purpose;building an efficient system;getting the message out and sharing information;understanding roles and support and training of staff;building capacity and systems change;addressing service gaps;and engaging ***

关键词： Partners in Recovery Mental health program logic Mixed methods Australia

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：