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

30th International Symposium on Model Checking software

作者： Ayaziova, Paulina Beyer, Dirk Lingsch-Rosenfeld, Marian Spiessl, Martin Strejcek, Jan Masaryk Univ Brno Czech Republic Ludwig Maximilians Univ Munchen Munich Germany

ISBN: (纸本)9783031661488;9783031661495

verification witnesses are now widely accepted objects used not only to confirm or refute verification results, but also for general exchange of information among various tools for program verification. The original format for witnesses is based on GraphML, and it has some known issues including a semantics based on control-flow automata, limited tool support of some format features, and a large size of witness files. This paper presents version 2.0 of the witness format, which is based on YAML and overcomes the above-mentioned issues. We describe the new format, provide an experimental comparison of various aspects of the original and the new witness format showing that both witness formats perform similarly, and report on its adoption in the community.

关键词： verification Witness software verification Validation Exchange Format Invariant Counterexample

来源：评论

学校读者我要写书评

暂无评论

software verification with CPAchecker 3.0: Tutorial and User Guide 26th

Software Verification with CPAchecker 3.0: Tutorial and User...

引用

26th International Symposium on Formal Methods (FM)

作者： Baier, Daniel Beyer, Dirk Chien, Po-Chun Jakobs, Marie-Christine Jankola, Marek Kettl, Matthias Lee, Nian-Ze Lemberger, Thomas Lingsch-Rosenfeld, Marian Wachowitz, Henrik Wendler, Philipp Ludwig Maximilians Univ Munchen Munich Germany

ISBN: (纸本)9783031711763;9783031711770

This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://***/***.

关键词： CPAchecker Configurable Program Analysis Formal verification Model Checking software verification Program Analysis Testing Tutorial Correctness Certification Witnesses Witness Validation Fault Visualization

来源：评论

学校读者我要写书评

暂无评论

Interpolation and SAT-Based Model Checking Revisited: Adoption to software verification

引用

JOURNAL OF AUTOMATED REASONING 2025年第1期69卷 1-29页

作者： Beyer, Dirk Lee, Nian-Ze Wendler, Philipp Ludwig Maximilians Univ Munchen Munich Germany

The article Interpolation and SAT-Based Model Checking (McMillan in: Proc. CAV 2003, LNCS, Springer [56]) describes a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. It derives interpolants from unsatisfiable BMC queries and collects them to construct an overapproximation of the set of reachable states. Although 20 years old, the algorithm is still state-of-the-art in hardware model checking. Unlike other formal-verification algorithms, such as or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's interpolation-based model-checking algorithm from 2003 has not been used to verify programs so far. Our contribution is to close this significant, two decades old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker and evaluated the implementation against other state-of-the-art software-verification techniques on the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that McMillan's interpolation-based model-checking algorithm from 2003 is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results are important for the area of software verification, because researchers and developers now have one more approach to choose from.

关键词： software verification Program analysis Model checking Interpolation Interpolation-based model checking CPAchecker SMT SAT

来源：评论

学校读者我要写书评

暂无评论

software verification challenges in the blockchain ecosystem

引用

INTERNATIONAL JOURNAL ON software TOOLS FOR TECHNOLOGY TRANSFER 2024年第4期26卷 431-444页

作者： Olivieri, Luca Spoto, Fausto CaFoscari Univ Venice Venice Italy Univ Verona Verona Italy

Blockchain technology has created a new software development context, with its own peculiarities, mainly due to the guarantees that the technology must satisfy, that is, immutability, distributability, and decentralization of data. Its rapid evolution over the last decade implied a lack of adequate verification tools, exposing developers and users to critical vulnerabilities and bugs. This paper clarifies the extent of block chain-oriented software (BoS), that goes well beyond smart contracts. Moreover, it provides an overview of the challenges related to software verification in the blockchain context, encompassing smart contracts, blockchain layers, cross-chain applications, and, more generally, BoS. This study aims to highlight the shortcomings of the state-of-art and of the state-of-practice of software verification in that context and identify, at the same time, new research directions.

关键词： Blockchain Smart contracts Blockchain-oriented software software verification Program analysis Automatic verification

来源：评论

学校读者我要写书评

暂无评论

software verification and graph similarity for automated evaluation of students' assignments

引用

INFORMATION AND software TECHNOLOGY 2013年第6期55卷 1004-1016页

作者： Vujosevic-Janicic, Milena Nikolic, Mladen Tosic, Dugan Kuncak, Viktor Univ Belgrade Fac Math Belgrade 11000 Serbia Ecole Polytech Fed Lausanne Sch Comp & Commun Sci Stn 14 CH-1015 Lausanne Switzerland

Context: The number of students enrolled in universities at standard and on-line programming courses is rapidly increasing. This calls for automated evaluation of students assignments. Objective: We aim to develop methods and tools for objective and reljable automated grading that can also provide substantial and comprehensible feedback. Our approach targets introductory programming courses, which have a number of specific features and goals. The benefits are twofold: reducing the workload for teachers, and providing helpful feedback to students in the process of learning. Method: For sophisticated automated evaluation of students' programs, our grading framework combines results of three approaches (i) testing, (ii) software verification, and (iii) control flow graph similarity measurement. We present our tools for software verification and control flow graph similarity measurement, which are publicly available and open source. The tools are based on an intermediate code representation, so they could be applied to a number of programming languages. Results: Empirical evaluation of the proposed grading framework is performed on a corpus of programs written by university students in programming language C within an introductory programming course. Results of the evaluation show that the synergy of proposed approaches improves the quality and precision of automated grading and that automatically generated grades are highly correlated with instructor-assigned grades. Also, the results show that our approach can be trained to adapt to teacher's grading style. Conclusions: In this paper we integrate several techniques for evaluation of student's assignments. The obtained results suggest that the presented tools can find real-world applications in automated grading. (C) 2012 Elsevier B.V. All rights reserved.

关键词： Automated grading software verification Graph similarity Computer supported education

来源：评论

学校读者我要写书评

暂无评论

software verification and Validation Technologies and Tools

引用

IEEE software 2019年第2期36卷 13-24页

作者： Rodriguez, Moises Piattini, Mario Ebert, Christof AQCLab Ciudad Real Spain Univ Castilla La Mancha Ciudad Real Spain Alarcos Res Grp Ciudad Real Spain Univ Stuttgart Stuttgart Germany Sorbonne Paris Paris France

software quality matters-more than ever. software has become the most crucial infrastructure in this century. All businesses is software businesses because they based their operations and services in the Internet of Things, business intelligence (BI), artificial intelligence, cloud computing, social networks, and so forth. Classic IT and embedded systems are converging toward ubiquitous software. Systems will be connected and thus increasingly missing critical. The digital transformation across industries depends on systems performing according to their requirements and needs. This importance of software quality has grown considerably over recent years.

关键词： Artificial Intelligence Cloud Computing Competitive Intelligence Embedded Systems Internet Social Networking Online software Quality Ubiquitous Computing Ubiquitous software software verification Crucial Infrastructure software Businesses Internet Of Things Artificial Intelligence Cloud Computing Social Networks Classic IT Embedded Systems software Quality software Testing ISO Standards Static Analysis software Quality Quality Assessment

来源：评论

学校读者我要写书评

暂无评论

software verification with VeriFast: Industrial case studies

引用

SCIENCE OF COMPUTER PROGRAMMING 2014年 82卷 77-97页

作者： Philippaerts, Pieter Muhlberg, Jan Tobias Penninckx, Willem Smans, Jan Jacobs, Bart Piessens, Frank Katholieke Univ Leuven iMinds DistriNet B-3001 Louvain Belgium

In this article, we present a series of four industrial case studies in software verification. We applied VeriFast, a sound and modular software verifier based on separation logic, to two Java Card smart card applets, a Linux device driver, and an embedded Linux network management component, the latter two written in C. Our case studies have been carefully selected so as to evaluate the industrial applicability of VeriFast. We focus on proving the absence of safety violations, e.g., that the programs do not perform illegal operations such as dividing by zero or illegal memory accesses. Yet, given the sensitive application environment of our case studies, these safety properties typically have security implications. In this article we give a detailed description of the VeriFast approach to software verification based on two of the above case studies, one in Java and one in C. Finally, we draw conclusions on the overall feasibility of using VeriFast to verify software components in industrial domains that have stringent requirements on reliability and security. (C) 2013 Elsevier B.V. All rights reserved.

关键词： software verification Industrial case studies VeriFast

来源：评论

学校读者我要写书评

暂无评论

software verification with PDR: An Implementation of the State of the Art 26th

Software Verification with PDR: An Implementation of the Sta...

引用

26th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS)

作者： Beyer, Dirk Dangl, Matthias Ludwig Maximilians Univ Munchen Munich Germany

ISBN: (纸本)9783030451899;9783030451905

Property-directed reachability (PDR) is a SAT/SMT-based reachability algorithm that incrementally constructs inductive invariants. After it was successfully applied to hardware model checking, several adaptations to software model checking have been proposed. We contribute a replicable and thorough comparative evaluation of the state of the art: We (1) implemented a standalone PDR algorithm and, as improvement, a PDR-based auxiliary-invariant generator for k-induction, and (2) performed an experimental study on the largest publicly available benchmark set of C verification tasks, in which we explore the effectiveness and efficiency of software verification with PDR. The main contribution of our work is to establish a reproducible baseline for ongoing research in the area by providing a well-engineered reference implementation and an experimental evaluation of the existing techniques.

关键词： software verification Program analysis Invariant generation Property-directed reachability (PDR) IC3 k-Induction VVT CPAchecker

来源：评论

学校读者我要写书评

暂无评论

software verification: 10th Comparative Evaluation (SV-COMP 2021) 27th

Software Verification: 10th Comparative Evaluation (SV-COMP ...

引用

27th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS)

作者： Beyer, Dirk Ludwig Maximilians Univ Munchen Munich Germany

ISBN: (纸本)9783030720124;9783030720131

SV-COMP 2021 is the 10th edition of the Competition on software verification (SV-COMP), which is an annual comparative evaluation of fully automatic software verifiers for C and Java programs. The competition provides a snapshot of the current state of the art in the area, and has a strong focus on reproducibility of its results. The competition was based on 15 201 verification tasks for C programs and 473 verification tasks for Java programs. Each verification task consisted of a program and a property (reachability, memory safety, overflows, termination). SV-COMP 2021 had 30 participating verification systems from 27 teams from 11 countries.

关键词： Formal verification Program Analysis Competition software verification verification Tasks Benchmark C Language Java Language SV-Benchmarks

来源：评论

学校读者我要写书评

暂无评论

software verification of Autonomic Systems Developed with ASSL

引用

16th Monterey Workshop

作者： Vassev, Emil Hinchey, Mike Univ Limerick Lero Irish Software Engn Res Ctr Limerick Ireland

ISBN: (纸本)9783642212925

We discuss our experiences in building tools for software verification of autonomic systems developed with the Autonomic System Specification Language (ASSL). ASSL is a software framework that aims to assist developers of autonomic systems by providing a powerful combination of both notation and tools. One of the major objectives of the framework is to assure the correctness of the autonomic systems via inclusion of tools targeting consistency checking, model checking, and automatic test case generation. In this paper, we review our recent work on these tools.

关键词： software verification formal methods ASSL autonomic computing

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：