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

HIERARCHIES OF program logicS

引用

SIBERIAN MATHEMATICAL JOURNAL 1983年第3期24卷 469-476页

作者： TAITSLIN, MA

来源：评论

学校读者我要写书评

暂无评论

The next 700 relational program logics

The next 700 relational program logics

引用

Proceedings of the ACM on programming Languages

作者： Maillard, Kenji Hrit, Ctlin Rivas, Exequiel Van Muylder, Antoine Inria Paris ENS Paris France Université de Paris Paris France

We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic presentation of relational specifications as a class of relative monads, and link computations and specifications by introducing relational effect observations, which map pairs of monadic computations to relational specifications in a way that respects the algebraic structure. For an arbitrary relational effect observation, we generically define the core of a sound relational program logic, and explain how to complete it to a full-fledged logic for the monadic effect at hand. We show that this generic framework can be used to define relational program logics for effects as diverse as state, input-output, nondeterminism, and discrete probabilities. We, moreover, show that by instantiating our framework with state and unbounded iteration we can embed a variant of Benton's Relational Hoare logic, and also sketch how to reconstruct Relational Hoare Type Theory. Finally, we identify and overcome conceptual challenges that prevented previous relational program logics from properly dealing with control effects, and are the first to provide a relational program logic for exceptions. © 2020 Association for Computing Machinery. All rights reserved.

关键词： Computer circuits Algebra Formal languages Foundations Probability Semantics Specifications Dependent types Exceptions Monads Non determinism program logic program Verification Relative monads Side effect State

来源：评论

学校读者我要写书评

暂无评论

Verifying Contextual Refinement with Ownership Transfer

引用

Journal of Computer Science & Technology 2021年第6期36卷 1342-1366页

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

Contextual refinement is a compositional approach to compositional verification of concurrent *** has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract ***,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and *** this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership *** also design a program logic to verify contextual refinement of concurrent objects *** abstract *** have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.

关键词： contextual refinement program logic concurrent object ownership transfer verification

来源：评论

学校读者我要写书评

暂无评论

Deviation-Based Obfuscation-Resilient program Equivalence Checking With Application to Software Plagiarism Detection

引用

IEEE TRANSACTIONS ON RELIABILITY 2016年第4期65卷 1647-1664页

作者： Ming, Jiang Zhang, Fangfang Wu, Dinghao Liu, Peng Zhu, Sencun Penn State Univ Coll Informat Sci & Technol University Pk PA 16802 USA Penn State Univ Dept Comp Sci & Engn University Pk PA 16802 USA

Software plagiarism, an act of illegally copying others' code, has become a serious concern for honest software companies and the open source community. Considerable research efforts have been dedicated to searching the evidence of software plagiarism. In this paper, we continue this line of research and propose LoPD, a deviation-based program equivalence checking approach, which is an ideal fit for the whole-program plagiarism detection. Instead of directly comparing the similarity between two programs, LoPD searches for any dissimilarity between two programs by finding an input that will cause these two programs to behave differently, either with different output states or with semantically different execution paths. As long as we can find one dissimilarity, the programs are semantically different;but if we cannot find any dissimilarity, it is more likely a plagiarism case. We leverage dynamic symbolic execution to capture the semantics of execution paths and to find path deviations. Compared to the existing detection approaches, LoPD's formal program semantics-based method is more resilient to automatic obfuscation schemes. Our evaluation results indicate that LoPD is effective in detecting whole-program plagiarism. Furthermore, we demonstrate that LoPD can be applied to partial software plagiarism detection as well. The encouraging experiment results show that LoPD is an appealing complement to existing software plagiarism detection approaches.

关键词： Path deviation program logic semantical difference software plagiarism symbolic execution

来源：评论

学校读者我要写书评

暂无评论

Proof-carrying code from certified abstract interpretation and fixpoint compression

引用

THEORETICAL COMPUTER SCIENCE 2006年第3期364卷 273-291页

作者： Besson, Frederic Jensen, Thomas Pichardie, David Irisa F-35042 Rennes France

Proof-carrying code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's safety policy. We show how certified abstract interpretation can be used to build a PCC architecture where the code producer can produce program certificates automatically. Code consumers use proof checkers derived from certified analysers to check certificates. Proof checkers carry their own correctness proofs and accepting a new proof checker amounts to type checking the checker in Coq. Certificates take the form of strategies for reconstructing a fixpoint and are kept small due to a technique for fixpoint compression. The PCC architecture has been implemented and evaluated experimentally on a byte code language for which we have designed an interval analysis that allows to generate certificates ascertaining that no array-out-of-bounds accesses will occur. (C) 2006 Elsevier B.V. All rights reserved.

关键词： program logic data flow analysis abstract interpretation theorem proving computer security Java byte code

来源：评论

学校读者我要写书评

暂无评论

A SIMPLE DENOTATIONAL SEMANTICS, PROOF THEORY AND A VALIDATION CONDITION GENERATOR FOR UNIT-DELAY VHDL

引用

FORMAL METHODS IN SYSTEM DESIGN 1995年第1-2期7卷 27-51页

作者： BREUER, PT FERNANDEZ, LS KLOOS, CD UNIV POLITECN MADRID ETSI TELECOMMUNDEPT INGN SISTEMIS TELEMATE-28040 MADRIDSPAIN

A denotational semantics and a Hoare programming logic for a subset of the standard hardware description language VHDL are set out here. Both define the behaviour of synchronously clocked VHDL simulators in declarative and compositional style. The logic is proved complete with respect to the denotational semantics and a natural implementation of the logic in PROLOG as a validation condition generator for VHDL is also described. The subset of the language referred to above essentially consists of elaborated VHDL excluding only delta-delayed signal assignments and zero waits. However, for brevity, only one of the two forms of VHDL Signal assignment is treated here. Moreover, for simplicity, signal resolution functions and local state are assumed to have been encoded away via expressions and signals.

关键词： FORMAL VERIFICATION DIGITAL CIRCUITS DENOTATIONAL SEMANTICS VHDL program logic TIMED logic PROLOG

来源：评论

学校读者我要写书评

暂无评论

Evaluation Theory and Practice Applied to Cybersecurity Education

引用

IEEE SECURITY & PRIVACY 2015年第2期13卷 75-80页

作者： Dark, Melissa Mirkovic, Jelena Purdue Univ Coll Technol Technol W Lafayette IN 47907 USA Univ So Calif Inst Informat Sci Los Angeles CA 90089 USA

As more institutions, organizations, schools, and programs launch cybersecurity education programs in an attempt to meet needs that are emerging in a rapidly changing environment, evaluation will be important to ensur... 详细信息

关键词： Computer Security Performance Evaluation Game Theory Reliability program logic Design Methodology Reliability Cybersecurity Evaluation Theory Evaluation Design Formative Evaluation Summative Evaluation Measurement Metrics program logic Validity

来源：评论

学校读者我要写书评

暂无评论

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

引用

SOFTWARE AND SYSTEMS MODELING 2016年第4期15卷 1117-1140页

作者： de Gouw, Stijn de Boer, Frank Ahrendt, Wolfgang Bubel, Richard CWI Amsterdam Netherlands SDL Fredhopper Amsterdam Netherlands Leiden Univ Amsterdam Netherlands Chalmers Univ Technol Gothenburg Sweden Tech Univ Darmstadt Dept Comp Sci Darmstadt Germany

We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.

关键词： Specification Verification program logic Dynamic logic Object creation

来源：评论

学校读者我要写书评

暂无评论

THE GUARDED LAMBDA-CALCULUS programMING AND REASONING WITH GUARDED RECURSION FOR COINDUCTIVE TYPES

引用

logicAL METHODS IN COMPUTER SCIENCE 2016年第3期12卷

作者： Clouston, Ranald Bizjak, Ales Grathwohl, Hans Bugge Birkedal, Lars Aarhus Univ Dept Comp Sci Aarhus Denmark

We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with Lob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Rutten's behavioural differential equations.

关键词： guarded recursion coinductive types typed lambda-calculus denotational semantics program logic

来源：评论

学校读者我要写书评

暂无评论

A Compositional Theory of Linearizability

引用

JOURNAL OF THE ACM 2024年第2期71卷 1-107页

作者： Vale, Arthur Oliveira Shao, Zhong Chen, Yixuan Yale Univ New Haven CT USA Yale Univ Dept Comp Sci POB 208285 New Haven CT 06520 USA

Compositionality is at the core of programming languages research and has become an important goal toward scalable verification of large systems. Despite that, there is no compositional account of linearizability, the gold standard of correctness for concurrent objects. In this article, we develop a compositional semantics for linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, and this is themain discovery of ourwork, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other. We use this new, and compositional, understanding of linearizability to revisit much of the theory of linearizability, providing novel, simple, algebraic proofs of the locality property and of an analogue of the equivalence with observational refinement. We show our techniques can be used in practice by connecting our semantics with a simple program logic that is nonetheless sound concerning this generalized linearizability.

关键词： Linearizability game semantics concurrency program logic

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：