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

Decidability of logic program semantics and applications to testing

JOURNAL OF LOGIC programMING 2000年第1-2期46卷 103-137页

作者： Ruggieri, S Univ Pisa Dipartimento Informat I-56125 Pisa Italy

In this paper, we investigate the decidability problem of logic program semantics and observables, focusing in particular on the least Herbrand model (or M-semantics), the L-semanties, and the L-semantics. We introduce bounded logic programs, and show that they coincide with programs such that every ground query has finitely many SLD-refutations via any selection rule, In particular, bounded programs strictly include the well-studied class of acceptable logic programs. We show that the mentioned declarative semantics are decidable when considering acceptable programs and programs bounded by recursive level mappings. Interestingly, the decision procedures have direct implementations in the logic programming paradigm itself as Prolog meta-programs. We relate semantics decidability to program testing. In our terminology, the testing problem consists of checking whether or not the formal semantics of a program includes a given finite set of atoms. With this definition, semantics decidability and the testing problem are equivalent. The decision procedures are then recognized to be automatic tools for testing logic programs. The meta-programming approach reveals to be successful in modeling extensions such as arithmetic built-in's, negation, modular programming and some other declarative semantics. Also, we present some preliminary experimental results and an efficient compilation-oriented approach that overcome the overhead due to meta-programming. (C) 2000 Elsevier Science Inc. All rights reserved.

关键词： program semantics C and S-semantics testing bounded programs acceptable programs meta-interpreters

来源：评论

学校读者我要写书评

暂无评论

Learning program semantics for Vulnerability Detection via Vulnerability-Specific Inter-procedural Slicing 2023

Learning Program Semantics for Vulnerability Detection via V...

引用

31st ACM Joint Meeting of the European Software Engineering Conference / Symposium on the Foundations-of-Software-Engineering (ESEC/FSE)

作者： Wu, Bozhi Liu, Shangqing Xiao, Yang Li, Zhiming Sun, Jun Lin, Shang-Wei Singapore Management Univ Singapore Singapore Nanyang Technol Univ Singapore Singapore Chinese Acad Sci Beijing Peoples R China

ISBN: (纸本)9798400703270

Learning-based approaches that learn code representations for software vulnerability detection have been proven to produce inspiring results. However, they still fail to capture complete and precise vulnerability semantics for code representations. To address the limitations, in this work, we propose a learning-based approach namely SnapVuln, which first utilizes multiple vulnerability-specific inter-procedural slicing algorithms to capture vulnerability semantics of various types and then employs a Gated Graph Neural Network (GGNN) with an attention mechanism to learn vulnerability semantics. We compare SnapVuln with state-of-the-art learning-based approaches on two public datasets, and confirm that SnapVuln outperforms them. We further perform an ablation study and demonstrate that the completeness and precision of vulnerability semantics captured by SnapVuln contribute to the performance improvement.

关键词： Vulnerability detection program semantics code representations

来源：评论

学校读者我要写书评

暂无评论

An intelligent tutoring system for program semantics

An intelligent tutoring system for program semantics

引用

International Conference on Information Technology - Coding and Computing

作者： Barker, S Douglas, P Univ London Kings Coll London WC2R 2LS England

ISBN: (纸本)0769523153

In this paper, we describe an item of e-learning software that is intended to help students taking university computer science courses to understand the fundamentals of logic programming and deductive database semantics. The software is implemented in PROLOG and empowers students to explore their understanding of the semantics of logic programs and deductive databases. The software is also able to intelligently diagnose student misconceptions and includes a number of example programs/databases that permit students to test their understanding. We describe the development and evaluation of the software, and we present details of the analysis of the results of our investigation into the effectiveness of our e-learning tool. The results of our field study of the e-learning tool suggests that it of value in helping students to understand program and database semantics.

关键词： e-learning educational software program semantics

来源：评论

学校读者我要写书评

暂无评论

Auto-Generating Visual Exercises for Learning program semantics 19

Auto-Generating Visual Exercises for Learning Program Semant...

引用

ACM Conference on Innovation and Technology in Computer Science Education (ITiCSE)

作者： Smith, Rebecca Tang, Terry Warren, Joe Rixner, Scott Rice Univ Houston TX 77251 USA

ISBN: (纸本)9781450363013

Understanding program execution is a challenging task for novice programmers. The semantic rules which determine how execution affects the program state are numerous and complex, and students frequently hold fundamental misconceptions about these rules. If students do not build a correct mental model of program execution early on, they will face substantial hurdles as they try to develop and debug their code. This paper presents VizQuiz, a tool for auto generating multiple choice quizzes designed to help students gain insight into the semantic rules which govern program execution. VizQuiz provides students with an initial state and a piece of code, and tasks them with mentally tracing the execution of that code and selecting the correct final state. Reference diagrams are used to depict the initial and final states, and as feedback to help students visualize the correct behavior if they select a wrong answer. Feedback is auto -generated, so students can immediately correct their misconceptions and re-attempt.

关键词： Education program semantics program mutation

来源：评论

学校读者我要写书评

暂无评论

Unification of Four Versions of program semantics

引用

Formal Aspects of Computing 1998年第1期10卷 1-29页

作者： Rewitzky, Ingrid Brink, Chris Dept. of Math. and Appl. Mathematics University of Cape Town South Africa Dept. of Math. and Appl. Mathematics University of Cape Town Rondebosch 7700 Private Bag South Africa

In this paper we use Priestley duality and Jónsson/ Tarski duality to translate between four versions of program semantics: the relational model, predicate transformer semantics, information systems, and powerdomains. Our point of entry is the relational model, a kind of Kripke semantics, in which programs are thought of as input-output relations over a structured state space. Specifically, we present the state space as a certain kind of Priestley space, and programs as certain structure-preserving relations over such a space. We then derive, in circular fashion, a predicate transformer semantics from the relational model, an information system from the predicate transformer semantics, a powerdomain from the information system, and the original relational model back again from the powerdomain. The information system is also shown to be related to Hoare logic. To clarify the intuition behind this approach we present a case study, which is a 'Priestley version' of the so-called universal domain due to Plotkin, and we explicate various ideas about properties of programs and predicates in terms of this case study.

关键词： Hoare logic Information system Jónsson/Tarski duality Powerdomain Predicate transformer semantics Priestley duality program semantics Relational model

来源：评论

学校读者我要写书评

暂无评论

A trajectory-based strict semantics for program slicing

引用

THEORETICAL COMPUTER SCIENCE 2010年第11-13期411卷 1372-1386页

作者： Barraclough, Richard W. Binkley, David Danicic, Sebastian Harman, Mark Hierons, Robert M. Kiss, Akos Laurence, Mike Ouarbya, Lahcen Univ London Goldsmiths Coll Dept Comp London SE14 6NW England Loyola Coll Dept Comp Sci Baltimore MD 21210 USA Kings Coll London Dept Comp Sci London WC2R 2LS England Brunel Univ Sch Informat Syst Comp & Math Uxbridge UB8 3PH Middx England Univ Szeged Inst Informat Dept Software Engn H-6720 Szeged Hungary

We define a program semantics that is preserved by dependence-based slicing algorithms. It is a natural extension, to non-terminating programs, of the semantics introduced by Weiser (which only considered terminating ones) and, as such, is an accurate characterisation of the semantic relationship between a program and the slice produced by these algorithms. Unlike other approaches, apart from Weiser's original one, it is based on strict standard semantics which models the 'normal' execution of programs on a von Neumann machine and, thus, has the advantage of being intuitive. This is essential since one of the main applications of slicing is program comprehension. Although our semantics handles nontermination, it is defined wholly in terms of finite trajectories, without having to resort to complex, counter-intuitive, non-standard models of computation. As well as being simpler, unlike other approaches to this problem, Our semantics is substitutive. Substitutivity is an important property because it greatly enhances the ability to reason about correctness of meaning-preserving program transformations such as slicing. (C) 2009 Elsevier B.V. All rights reserved.

关键词： program slicing program semantics Non-termination program dependence

来源：评论

学校读者我要写书评

暂无评论

An SMT-Based Approach to the Verification of Knowledge-Based programs

引用

FORMAL ASPECTS OF COMPUTING 2025年第1期37卷 1-24页

作者： Belardinelli, Francesco Boureanu, Ioana Malvone, Vadim Rajaona, Fortunat Imperial Coll London London England Univ Surrey Guildford England Inst Polytech Paris Telecom Paris Paris France

We give a general-purpose programming language in which programs can reason about their own knowledge. To specify what these intelligent programs know, we define a "program epistemic" logic, akin to a dynamic epistemic logic for programs. Our logic properties are complex, including programs introspecting into future state of affairs, i.e., reasoning now about facts that hold only after they and other threads will execute. To model aspects anchored in privacy, our logic is interpreted over partial observability of variables, thus capturing that each thread can "see" only a part of the global space of variables. We verify programepistemic properties on such AI-centred programs. To this end, we give a sound translation of the validity of our program-epistemic logic into first-order validity, using a new weakest-precondition semantics and a book-keeping of variable assignment. We implement our translation and fully automate our verification method for well-established examples using SMT solvers.

关键词： Model Checking Epistemic Logic Epistemic Predicate Transformers program semantics

来源：评论

学校读者我要写书评

暂无评论

Reinvent Cloud Software Stacks for Resource Disagggiregation

引用

Journal of Computer Science & Technology 2023年第5期38卷 949-969页

作者：王晨曦单一舟左鹏飞崔慧敏 Institute of Computing Technology Chinese Academy of SciencesBeijing 100190China University of the Chinese Academy of Sciences Beijing 101408China Huawei Cloud Shenzhen 518129China

Due to the unprecedented development of low-latency interconnect technology,building large-scale disaggre-gated architecture is drawing more and more attention from both industry and *** disaggregation is a new way to organize the hardware resources of datacenters,and has the potential to overcome the limitations,e.g.,low re-source utilization and low reliability,of conventional ***,the emerging disaggregated architecture brings severe performance and latency problems to the existing cloud *** this paper,we take memory disaggregation as an example to demonstrate the unique challenges that the disaggregated datacenter poses to the existing cloud software stacks,e.g.,programming interface,language runtime,and operating system,and further discuss the possible ways to rein-vent the cloud systems.

关键词： cloud computing resource disaggregation datacenter program semantics

来源：评论

学校读者我要写书评

暂无评论

A taint based approach for automatic reverse engineering of gray-box file formats

引用

SOFT COMPUTING 2016年第9期20卷 3563-3578页

作者： Cui, Baojiang Wang, Fuwei Hao, Yongle Wang, Lingyu Beijing Univ Posts & Telecommun Beijing Peoples R China Natl Engn Lab Mobile Network Secur Beijing Peoples R China China Informat Technol Secur Evaluat Ctr Beijing Peoples R China Concordia Univ Concordia Inst Informat Syst Engn Montreal PQ Canada

File format vulnerabilities have been highlighted in recent years, and the performance of fuzzing tests relies heavily on the knowledge of target formats. In this paper, we present systematic algorithms and methods to automatically reverse engineer input file formats. The methodology employs dynamic taint analysis to reveal implicit relational information between input file and binary procedures, which is used for the measurement of correlations among data bytes, format segmentation and data type inference. We have implemented a prototype, and its general tests on 10 well-published binary formats yielded an average of over 85 % successful identification rate, while more detailed structural information was unveiled beyond coarse granular format analysis. Besides, a practical pseudo-fuzzing evaluation method is discussed in accordance with real-world demands on security analysis, and the evaluation results demonstrated the practical effectiveness of our system.

关键词： Format reverse engineering program semantics Dynamic taint analysis Fuzzing tests

来源：评论

学校读者我要写书评

暂无评论

Probabilistic rely-guarantee calculus

引用

THEORETICAL COMPUTER SCIENCE 2016年第PartB期655卷 120-134页

作者： McIver, Annabelle Rabehaja, Tahiry Struth, Georg Macquarie Univ Dept Comp N Ryde NSW Australia Univ Sheffield Dept Comp Sci Sheffield S Yorkshire England

Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach that is based on a combination of probabilistic Kleene algebra with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rules built on top of that semantics. In particular, we show how to obtain bounds on probabilities of correctness by deriving quantitative extensions of rely-guarantee rules. The use of these rules is illustrated by a detailed verification of a simple probabilistic concurrent program: a faulty Eratosthenes sieve. (C) 2016 Elsevier B.V. All rights reserved.

关键词： Probabilistic programs Concurrency Rely-guarantee program verification program semantics Kleene algebra Event structures

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：