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

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

来源：评论

学校读者我要写书评

暂无评论

Formally Verified Interval Arithmetic and Its Application to program verification 12

Formally Verified Interval Arithmetic and Its Application to...

引用

IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)

作者： Brucker, Achim D. Cameron-Burke, Teddy Stell, Amy Univ Exeter Dept Comp Sci Exeter Devon England

ISBN: (纸本)9798400705892

Interval arithmetic is a well known mathematical technique to analyse or mitigate rounding or measurement errors. Thus, it is promising to integrate interval analysis into program verification environments. Such an integration is not only useful for the verification of numerical algorithms: the need to ensure that computations stay within certain bounds is common. For example, to show that arithmetic computations stay within the hardware bounds of a given number representation. We present a formalisation of (extended) interval arithmetic in Isabelle/HOL, including the concept of inclusion isotone (extended) interval analysis. The main result of this part is the formal proof that interval-splitting converges for Lipschitz-continuous interval isotone functions. We also show how interval types can be used for verifying programs in a C-like programming language.

关键词： Extended Interval Analysis program verification Formalising Mathematics Isabelle/HOL

来源：评论

学校读者我要写书评

暂无评论

Slicing Assisted program verification: An Empirical Study 18th

Slicing Assisted Program Verification: An Empirical Study

引用

18th International Conference on Theoretical Aspects of Software Engineering (TASE)

作者： Chai, Wenjian Yan, Rongjie Zhang, Wenhui Zhang, Jian ISCAS Key Lab Syst Software CAS Beijing Peoples R China ISCAS State Key Lab Comp Sci Beijing Peoples R China Univ Chinese Acad Sci Beijing Peoples R China

ISBN: (纸本)9783031646256;9783031646263

Simplifying programs before verification aims to reduce program complexity thus saving the verification effort. In the paper, we investigate the impacts of applying program slicing before verification. We consider various techniques and verifiers for the workflow and adopt benchmarks from the software verification community to evaluate the strengths and issues in adopting slicing techniques for program simplification. The evaluation considers reachability as the property to be verified and checks the consistency of verification results, the improvement of verification efficiency, and the advantages of different toolchains when verifying reachability. The investigation shows that most programs keep consistent verification results after slicing and verifying programs with much code unrelated to the properties becomes faster when slicing is applied before verification. However, it is surprising that verification time for some programs can be significantly longer after slicing. We have investigated the reasons for such phenomenon concerning the features of these programs, and provide insightful conclusions obtained from using the slicing+verification approach.

关键词： Slicing program verification Reachability

来源：评论

学校读者我要写书评

暂无评论

Analysis and Transformation of Constrained Horn Clauses for program verification

引用

THEORY AND PRACTICE OF LOGIC programMING 2022年第6期22卷 974-1042页

作者： De Angelis, Emanuele Fioravanti, Fabio Gallagher, John P. Hermenegildo, Manuel, V Pettorossi, Alberto Proietti, Maurizio IASI CNR Rome Italy Univ G DAnnunzio DEC Chieti Italy Roskilde Univ Roskilde Denmark IMDEA Software Inst Madrid Spain Univ Politecn Madrid UPM Madrid Spain Univ RomeTor Vergata DICII Rome Italy

This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialization-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialization and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.

关键词： program verification program analysis program transformation constrained Horn clauses constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

Correct approximation of IEEE 754 floating-point arithmetic for program verification

引用

CONSTRAINTS 2022年第1-2期27卷 29-69页

作者： Bagnara, Roberto Bagnara, Abramo Biselli, Fabio Chiari, Michele Gori, Roberta Univ Parma Dipartimento Sci Matemat Fis & Informat Parma Italy BUGSENG Srl Parma Italy Certus Software V&V Ctr SIMULA Res Lab Fornebu Norway Politecn Milan Dipartimento Elettron Informaz & Bioingn Milan Italy Univ Pisa Dipartimento Informat Pisa Italy

verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects (NaNs), signed zeroes, denormal numbers, different rounding modes, etc. One possibility to reason about floating-point arithmetic is to model a program computation path by means of a set of ternary constraints of the form and use constraint propagation techniques to infer new information on the variables' possible values. In this setting, we define and prove the correctness of algorithms to precisely bound the value of one of the variables x, y or z, starting from the bounds known for the other two. We do this for each of the operations and for each rounding mode defined by the IEEE 754 binary floating-point standard, even in the case the rounding mode in effect is only partially known. This is the first time that such so-called filtering algorithms are defined and their correctness is formally proved. This is an important slab for paving the way to formal verification of programs that use floating-point arithmetics.

关键词： Constraint solving Constraint propagation Constraint satisfaction problem Filtering algorithm Floating point program verification Symbolic execution

来源：评论

学校读者我要写书评

暂无评论

Execution Time program verification with Tight Bounds 25th

Execution Time Program Verification with Tight Bounds

引用

25th International Symposium on Practical Aspects of Declarative Languages (PADL)

作者： Silva, Ana Carolina Barbosa, Manuel Florido, Mario Univ Porto Fac Ciencias Porto Portugal INESC TEC Porto Portugal Univ Porto LIACC Porto Portugal

ISBN: (纸本)9783031248405;9783031248412

This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time reasoning, and less pessimistic execution time estimation using amortized analysis. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. Finally, we define a verification conditions (VC) generator that generates the goals needed to prove program correctness, cost, and termination. Those goals are then sent to the Easycrypt toolset for validation. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs. Our case studies are motivated by real-time and cryptographic software.

关键词： program verification Execution time analysis Amortized analysis Hoare logic

来源：评论

学校读者我要写书评

暂无评论

Consistency-Preserving Propagation for SMT Solving of Concurrent program verification

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2022年第OOPSLA期6卷 929–956页

作者： Sun, Zhihang Fan, Hongyu He, Fei Tsinghua Univ Sch Software Beijing Peoples R China

The happens-before orders have been widely adopted to model thread interleaving behaviors of concurrent programs. A dedicated ordering theory solver, usually composed of theory propagation, consistency checking, and conflict clause generation, plays a central role in concurrent program verification. We propose a novel preventive reasoning approach that automatically preserves the ordering consistency and makes consistency checking and conflict clause generation omissible. We implement our approach in a prototype tool and conduct experiments on credible benchmarks;results reveal a significant improvement over existing state-of-the-art concurrent program verifiers.

关键词： program verification concurrent programs memory model satisfiability modulo theories

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Modelling program verification Tools for Software Engineers 22

Modelling Program Verification Tools for Software Engineers

引用

ACM/IEEE 25th International Conference on Model Driven Engineering Languages and Systems (MODELS)

作者： Lathouwers, Sophie Zaytsev, Vadim Univ Twente Enschede Netherlands

ISBN: (纸本)9781450394666

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 almost 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 categorisation enables software engineers to find suitable tools, investigate similar alternatives and compare them. We also identify trends for each level in our megamodel based on the categorisation. 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.

关键词： Formal Methods program verification Megamodelling

来源：评论

学校读者我要写书评

暂无评论

Interference Relation-Guided SMT Solving for Multi-Threaded program verification 22

Interference Relation-Guided SMT Solving for Multi-Threaded ...

引用

27th ACM SIGPLAN Symposium on Principles and Practice of Parallel programming (PPoPP)

作者： Fan, Hongyu Liu, Weiting He, Fei Tsinghua Univ Sch Software Key Lab Informat Syst Secur MoE Beijing Natl Res Ctr Informat Sci & Technol Beijing Peoples R China

ISBN: (纸本)9781450392044

Concurrent program verification is challenging due to a large number of thread interferences. A popular approach is to encode concurrent programs as SMT formulas and then rely on off-the-shelf SMT solvers to accomplish the verification. In most existing works, an SMT solver is simply treated as the backend. There is little research on improving SMT solving for concurrent program verification. In this paper, we recognize the characteristics of interference relation in multi-threaded programs and propose a novel approach for utilizing the interference relation in the SMT solving of multi-threaded program verification under various memory models. We show that the backend SMT solver can benefit a lot from the domain knowledge of concurrent programs. We implemented our approach in a prototype tool called ZPRE. We compared it with the state-of-the-art Z3 tool on credible benchmarks from the ConcurrencySafety category of SV-COMP 2019. Experimental results show promising improvements attributed to our approach.

关键词： Concurrent programs program verification Satisfiability modulo theory Partial order Weak memory models

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：