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

Extract, model, refine: improved modelling of program verification tools through data enrichment

SOFTWARE AND SYSTEMS MODELING 2025年 1-21页

作者： Lathouwers, Sophie Liu, Yujie Zaytsev, Vadim Univ Twente Formal Methods & Tools Enschede Netherlands

In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools and present a concise megamodel to distinguish these tools. We also present a data set of 400+ program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input/output format, repository links and more. The practical information, such as last commit date, is kept up to date through the use of APIs. Moreover, part of the data extraction has been automated to make it easier to expand the data set. The categorisation enables software engineers to find suitable tools, investigate alternatives and compare tools. We also identify trends for each level in our megamodel. Our data set, publicly available at https://***/10.4121/20347950, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements. This paper is an extended version of https://***/10.1145/3550355.3552426.

关键词： program verification Megamodelling Data enrichment Data extraction

来源：评论

学校读者我要写书评

暂无评论

Towards neural-network-guided program synthesis and verification

引用

FORMAL METHODS IN SYSTEM DESIGN 2025年 1-33页

作者： Kobayashi, Naoki Sekiyama, Taro Sato, Issei Unno, Hiroshi Univ Tokyo Tokyo Japan Natl Inst Informat SOKENDAI Tokyo Japan Tohoku Univ Sendai Japan

We propose a novel framework of program and invariant synthesis called neural network-guided synthesis (NeuGuS). We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks. Based on the idea, we have implemented a tool to synthesize formulas from positive/negative examples and implication constraints, and obtained promising experimental results. We also discuss two applications of our synthesis method. One is the use of our tool for qualifier discovery in the framework of ICE-learning-based CHC solving, which can in turn be applied to program verification and inductive invariant synthesis. Another application is to a new program development framework called oracle-based programming, which is a neural-network-guided variation of Solar-Lezama's program synthesis by sketching.

关键词： program verification program synthesis Neural network

来源：评论

学校读者我要写书评

暂无评论

program verification AND ADA

引用

IEE PROCEEDINGS-E COMPUTERS AND DIGITAL TECHNIQUES 1982年第2期129卷 55-62页

作者： MCGETTRICK, AD Department of Computer Science University of Strathclyde Glasgow UK

One of the design aims of Ada was to provide a language which would encourage the production of reliable programs: An important technique used to provide greater reliability is program verification. In this paper, we comment on the design of Ada from this particular point of view and we indicate particular approaches to the verification of Ada programs.

关键词： program verification Ada programs Ada High level languages programming theory programming and algorithm theory verification

来源：评论

学校读者我要写书评

暂无评论

program verification using symbolic game semantics

引用

THEORETICAL COMPUTER SCIENCE 2014年第Part3期560卷 364-379页

作者： Dimovski, Aleksandar S. FON Univ Fac Informat Commun Tech Skopje 1000 North Macedonia

We introduce a new symbolic representation of algorithmic game semantics, and show how it can be applied for efficient verification of open (incomplete) programs. The focus is on an Algol-like programming language which contains the core ingredients of imperative and functional languages, especially on its second-order recursion-free fragment with infinite data types. We revisit the regular-language representation of game semantics of this language fragment. By using symbolic values instead of concrete ones, we generalize the standard notions of regular-language and automata representations of game semantics to those of corresponding symbolic representations. In this way programs with infinite data types, such as integers, can be expressed as finite-state symbolic-automata although the standard automata representation is infinite-state, i.e. the standard regular-language representation has infinite summations. Moreover, in this way significant reductions of the state space of game semantics models are obtained. This enables efficient verification of programs by our prototype tool based on symbolic game models, which is illustrated with several examples. (C) 2014 Elsevier B.V. All rights reserved.

关键词： Algorithmic game semantics Symbolic automata program verification Predicate abstraction

来源：评论

学校读者我要写书评

暂无评论

program verification using Constraint Handling Rules and Array Constraint Generalizations

引用

FUNDAMENTA INFORMATICAE 2017年第1期150卷 73-117页

作者： De Angelis, Emanuele Pettorossi, Alberto Fioravanti, Fabio Proietti, Maurizio Univ G dAnnunzio Viale Pindaro 42 I-65127 Pescara Italy Univ Roma Tor Vergata Via Politecn 1 I-00133 Rome Italy CNR IASI Via Taurini 19 I-00185 Rome Italy

The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program progas a predicate incorrect defined by a CLP program T, and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs thatmanipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

关键词： Constraint Handling Rules Constraint logic programming program transformation program verification

来源：评论

学校读者我要写书评

暂无评论

program verification and Functioning of Operative Computing Revisited: How about Mathematics Engineering?

引用

MINDS AND MACHINES 2011年第2期21卷 337-359页

作者： Pincas, Uri Open Univ Israel Raanana Israel

The issue of proper functioning of operative computing and the utility of program verification, both in general and of specific methods, has been discussed a lot. In many of those discussions, attempts have been made to take mathematics as a model of knowledge and certitude achieving, and accordingly infer about the suitable ways to handle computing. I shortly review three approaches to the subject, and then take a stance by considering social factors which affect the epistemic status of both mathematics and computing. I use the analogy between mathematics and computing in reverse-that is to say, I consider operative computing as a form of making mathematics, and so attempt to learn from computing to mathematics in general. I conclude that "mathematics engineering" is a field to be both developed for practical improvement of doing mathematics and taken into consideration while philosophizing about mathematics as well.

关键词： Computing engineering Operative computing Philosophy of mathematics program verification Software engineering

来源：评论

学校读者我要写书评

暂无评论

program verification by using DISCOVERER

引用

1st Working Conference on Verified Software - Theories, Tools and Experiments (VSTTE 2005)

作者： Yang, Lu Zhan, Naijun Xia, Bican Zhou, Chaochen East China Normal Univ Inst Software Engn Shanghai Peoples R China Acad Sinica Comp Sci Lab Inst Software Taipei Taiwan Peking Univ Sch Math Sci LMAM Beijing Peoples R China

ISBN: (纸本)9783540691471

Recent advances in program verification indicate that various verification problems can be reduced to semi-algebraic system (SAS for short) solving. An SAS consists of polynomial equations and polynomial inequalities. Algorithms for quantifier elimination of real closed fields are the general method for those problems. But the general method usually has low efficiency for specific problems. To overcome the bottleneck of program verification with a symbolic approach, one has to combine special techniques with the general method. Based on the work of complete discrimination systems of polynomials [33,31], we invented new theories and algorithms [32,30,35] for SAS solving and partly implemented them as a real symbolic computation tool in Maple named DISCOVERER. In this paper, we first summarize the results that we have done so far both on SAS-solving and program verification with DISCOVERER, and then discuss the future work in this direction, including SAS-solving itself, termination analysis and invariant generation of programs, and reachability computation of hybrid systems etc.

关键词： semi-algebraic systems DISCOVERER program verification termination invariant generation reachability computation

来源：评论

学校读者我要写书评

暂无评论

program verification by Reduction to Semi-algebraic Systems Solving

Program Verification by Reduction to Semi-algebraic Systems ...

引用

3rd International Symposium on Leveraging Applications of Formal Methods, verification and Validation

作者： Xia, Bican Yang, Lu Zhan, Naijun Peking Univ LMAM Sch Math Sci Beijing Peoples R China East China Normal Univ Shanghai Key Lab Trustworthy Comp Shanghai Peoples R China Chinese Acad Sci Inst Software Comp Sci Lab Beijing 100864 Peoples R China

ISBN: (纸本)9783540884781

The discovery of invariants and ranking functions plays a central role in program verification. In our previous work, we investigated invariant generation and non-linear ranking function discovering of polynomial programs by reduction to semi-algebraic systems solving. In this paper we will first summarize our results on the two topics and then show how to generalize the approach to discovering more expressive invariants and ranking functions, and applying to more general programs.

关键词： program verification Ranking Functions Invariants Polynomial programs Semi-Algebraic Systems Quantifier Elimination

来源：评论

学校读者我要写书评

暂无评论

program verification Under Weak Memory Consistency Using Separation Logic 29th

Program Verification Under Weak Memory Consistency Using Sep...

引用

29th International Conference on Computer-Aided verification (CAV)

作者： Vafeiadis, Viktor SWS MPI Saarbrucken Germany

ISBN: (纸本)9783319633879;9783319633862

The semantics of concurrent programs is now defined by a weak memory model, determined either by the programming language (e.g., in the case of C/C++11 or Java) or by the hardware architecture (e.g., for assembly and legacy C code). Since most work in concurrent software verification has been developed prior to weak memory consistency, it is natural to ask how these models affect formal reasoning about concurrent programs. In this overview paper, we show that verification is indeed affected: for example, the standard Owicki-Gries method is unsound under weak memory. Further, based on concurrent separation logic, we develop a number of sound program logics for fragments of the C/C++11 memory model. We show that these logics are useful not only for verifying concurrent programs, but also for explaining the weak memory constructs of C/C++.

关键词： Parallel programming program verification Formal logic Memory Memory Semantics verification Java Java programming language

来源：评论

学校读者我要写书评

暂无评论

program verification Enhanced Precise Analysis of Interrupt-Driven program Vulnerabilities 28

Program Verification Enhanced Precise Analysis of Interrupt-...

引用

28th Asia-Pacific Software Engineering Conference (APSEC)

作者： Du, Xiang Yin, Liangze Feng, Haining Dong, Wei Natl Univ Def Technol Lab Software Engn Complex Syst Changsha Peoples R China

ISBN: (纸本)9781665437844

Due to the non-deterministic occurring of interrupt service routines, vulnerabilities of interrupt-driven programs, such as data race and atomicity violation, are usually hard to discover. Static analysis is an effective method for vulnerability analysis of interrupt-driven programs. However, existing techniques usually produce a large number of false alarms, which limits the application of static analysis in practice. To achieve high precision in vulnerability analysis of interrupt-driven programs, this paper proposes a program verification enhanced precise analysis method. For each potential vulnerability detected by static analysis, we propose a vulnerability validation approach which employs program verification to further automatically verify its feasibility. We have implemented a prototype of our method on top of CBMC. Experimental results on both an academic benchmark and 24 real-world programs show that our method can successfully identify true vulnerabilities and achieve a high precise analysis.

关键词： Interrupt driven programs Data Race Atomicity Violation Static Analysis program verification

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：