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

36th International Conference on Computer-Aided Verification (CAV)

作者： Abate, Alessandro Giacobbe, Mirco Schnitzer, Yannik Univ Oxford Oxford England Univ Birmingham Birmingham W Midlands England

ISBN: (纸本)9783031656323;9783031656330

We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the problem of learning a state classifier together with a ranking function for each class. Our procedure learns a candidate state classifier and candidate ranking functions from a finite dataset of sample states;then, it checks whether these generalise to the entire state space using satisfiability modulo theory solving. Upon the affirmative answer, the procedure concludes that the classifier constitutes a valid stutter-insensitive bisimulation of the system. Upon a negative answer, the solver produces a counterexample state for which the classifier violates the claim, adds it to the dataset, and repeats learning and checking in a counterexample-guided inductive synthesis loop until a valid bisimulation is found. We demonstrate on a range of benchmarks from reactive verification and software model checking that our method yields faster verification results than alternative state-of-the-art tools in practice. Our method produces succinct abstractions that enable an effective verification of linear temporal logic without next operator, and are interpretable for system diagnostics.

关键词： Data-driven verification Stutter-insensitive bisimulation Reactive verification software model checking Abstraction

来源：评论

学校读者我要写书评

暂无评论

CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification 38

CPA-DF: A Tool for Configurable Interval Analysis to Boost P...

引用

38th IEEE/ACM International Conference on Automated software Engineering (ASE)

作者： Beyer, Dirk Chien, Po-Chun Lee, Nian-Ze Ludwig Maximilians Univ Munchen Munich Germany

ISBN: (纸本)9798350329964

software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the k-induction implementation in CPACHECKER, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on SV-Benchmarks, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain k-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain k-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized k-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPACHECKER, we use COVERITEAM, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA- DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20 %. Demonstration video: https://***/l7UG-vhTL_4

关键词： Data Flow Analysis Dynamic Precision Adjustment Interval Analysis Invariant Generation Program Analysis software model checking

来源：评论

学校读者我要写书评

暂无评论

Efficient Modular SMT-Based model checking of Pointer Programs 29th

Efficient Modular SMT-Based Model Checking of Pointer Progra...

引用

29th International Static Analysis Symposium (SAS)

作者： Garcia-Contreras, Isabel Gurfinkel, Arie Navas, Jorge A. Univ Waterloo Waterloo ON Canada Certora Seattle WA USA

ISBN: (纸本)9783031223075;9783031223082

Modularity is indispensable for scaling automatic verification to large programs. However, modularity also introduces challenges because it requires inferring and abstracting the behavior of functions as summaries - formulas that relate the function's inputs and outputs. For programs manipulating memory, summaries must include the function's frame, i.e., how the content memory is affected by the execution of the function. In SMT-based model-checking, memory is often modeled with (unbounded) logical arrays and expressing frames generally requires universally quantified formulas. Such formulas significantly complicate inference and subsequent reasoning and are thus to be avoided. In this paper, we present a technique to encode the memory that is bounded explicitly, eliminating the need for quantified summaries. We build on the insight that the size of frames can be statically known. This enables replacing unbounded arrays with finite maps - a finite collection of key-value pairs. Specifically, we develop a new static analysis to infer the finite parts of a function's frame. We then extend the theory of arrays to the theory of finite maps and show that satisfiability of Constrained Horn Clauses (CHCs) over finite maps is reducible to satisfiability of CHCs over the base theory. Finally, we propose a new encoding from imperative programs to CHCs that uses finite maps to model explicitly the finite memory passed in function calls. The result is a new verification strategy that preserves the advantages of modularity while reducing the need for quantified frames. We have implemented this approach in SEA-HORN, a state-of-the-art CHC-based software model checker for LLVM. An evaluation on Linux Drivers from SV-COMP shows the effectiveness of our technique.

关键词： Modular verification software model checking Constrained Horn clauses Pointer analysis

来源：评论

学校读者我要写书评

暂无评论

Prioritized Constraint-Aided Dynamic Partial-Order Reduction 7

Prioritized Constraint-Aided Dynamic Partial-Order Reduction

引用

37th IEEE/ACM International Conference on Automated software Engineering (ASE)

作者： Su, Jie Tian, Cong Yang, Zuchao Yang, Jiyu Yu, Bin Duan, Zhenhua Xidian Univ ICTT & ISN Lab Xian Peoples R China

ISBN: (纸本)9781450394758

Thread alternation aggravates the difficulty of concurrent program verification since the number of traces to be explored grows rapidly as the scale of a concurrent program increases. Partial-Order Reduction (POR) techniques alleviate the trace-space explosion problem by partitioning the traces into different equivalent classes. However, due to the coarse dependency approximation of transitions, there are still a large number of redundant traces explored throughout the verification. In this paper, a symbolic approach, namely Prioritized Constraint-Aided Dynamic Partial-Order Reduction (PC-DPOR), is proposed to reduce the redundant traces. Specifically, a constrained dependency graph is presented to refine dependencies between transitions, and the exploration of isolated transitions in the graph is prioritized to reduce redundant equivalent traces. Further, we utilize the generated constraints to dynamically detect whether the enabled transitions at the given reachable states are dependent, and thereby to overcome the inherent imprecision of the traditional dependence over-approximation. We have implemented the proposed approach as an extension of CPAchecker by utilizing BDDs as the representation of state sets. Experimental results show that our approach can effectively reduce the time and memory consumption for verifying concurrent programs. In particular, the number of explored states is reduced to 8.62% on average.

关键词： software model checking concurrent program verification symbolic model checking dynamic partial-order reduction

来源：评论

学校读者我要写书评

暂无评论

ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation 2022

ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermedi...

引用

31st ACM SIGSOFT International Symposium on software Testing and Analysis (ISSTA)

作者： Menezes, Rafael Moura, Daniel Cavalcante, Helena de Freitas, Rosiane Cordeiro, Lucas C. Univ Manchester Manchester Lancs England Univ Fed Amazonas Manaus Amazonas Brazil

ISBN: (纸本)9781450393799

We describe and evaluate the first model checker for verifying Kotlin programs through the Jimple intermediate representation. The verifier, named ESBMC-Jimple, is built on top of the Efficient SMT-based Context-Bounded model Checker (ESBMC). It uses the Soot framework to obtain the Jimple IR, representing a simplified version of the Kotlin source code, containing a maximum of three operands per instruction. ESBMC-Jimple processes Kotlin source code together with a model of the standard Kotlin libraries and checks a set of safety properties. Experimental results show that ESBMC-Jimple can correctly verify a set of Kotlin benchmarks from the literature;it is competitive with state-of-the-art Java bytecode verifiers. A demonstration is available at https://***/J6WhNfXvJNc.

关键词： Formal Verification software model checking Kotlin Jimple

来源：评论

学校读者我要写书评

暂无评论

Active Learning of Abstract System models from Traces using model checking

Active Learning of Abstract System Models from Traces using ...

引用

25th Design, Automation and Test in Europe Conference and Exhibition (DATE)

作者： Jeppu, Natasha Yogananda Melham, Tom Kroening, Daniel Univ Oxford Oxford England Amazon Inc London England

ISBN: (纸本)9783981926361

We present a new active model-learning approach to generating abstractions of a system implementation, as finite state automata (FSAs), from execution traces. Given an implementation and a set of observable system variables, the generated automata admit all system behaviours over the given variables and provide useful insight in the form of invariants that hold on the implementation. To achieve this, the proposed approach uses a pluggable model learning component that can generate an FSA from a given set of traces. Conditions that encode a completeness hypothesis are then extracted from the FSA under construction and used to evaluate its degree of completeness by checking their truth value against the system using software model checking. This generates new traces that express any missing behaviours. The new trace data is used to iteratively refine the abstraction, until all system behaviours are admitted by the learned abstraction. To evaluate the approach, we reverse-engineer a set of publicly available Simulink Stateflow models from their C implementations.

关键词： active model learning execution traces system abstraction software model checking

来源：评论

学校读者我要写书评

暂无评论

C for Yourself: Comparison of Front-End Techniques for Formal Verification 10

C for Yourself: Comparison of Front-End Techniques for Forma...

引用

10th IEEE/ACM International Conference on Formal Methods in software Engineering (FormaliSE)

作者： Bajczi, Levente Adam, Zsofia Molnar, Vince Budapest Univ Technol & Econ Dept Measurement & Informat Syst Budapest Hungary

ISBN: (纸本)9781450392877

With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide range of inputs in an efficient way by reusing solutions from existing compiler technologies such as Eclipse CDT or LLVM. Our experience suggests that well-established techniques in compiler technology are not necessarily beneficial to model checkers and sometimes can even hurt their performance. In this paper, we review the tools mature enough to participate in the software Verification Competition in terms of the employed analysis and frontend techniques. We find that successful tools do exhibit a bias toward certain combinations. We explore the theoretical reasons and suggest an adaptable approach for model checking frameworks. We validate our recommendations by implementing a new frontend for a model checking framework and show that it indeed benefits some of the algorithms.

关键词： software model checking Formal Verification CEGAR BMC LLVM

来源：评论

学校读者我要写书评

暂无评论

Decomposing software Verification using Distributed Summary Synthesis

Proceedings of the ACM on Software Engineering

引用

Proceedings of the ACM on software Engineering 2024年第FSE期1卷 1307-1329页

作者： Dirk Beyer Matthias Kettl Thomas Lemberger LMU Munich Munich Germany

There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries (block contracts) are computed — based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (computed from postconditions received from block predecessors, i.e., which program states reach this block) and violation conditions to check at the block exit (computed from violation conditions received from block successors, i.e., which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a postcondition or violation condition) is available from other blocks, the verification can decide to restart with this new information. We realize our approach on the basis of configurable program analysis and implement it for the verification of C programs in the widely used verifier CPAchecker. A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well, and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.

关键词： Block Summaries Contract Synthesis Decomposition Strategies Formal Verification Multi-process model checking Parallelization Program Analysis software model checking

来源：评论

学校读者我要写书评

暂无评论

Scaling Automatic Modular Verification

Scaling Automatic Modular Verification

引用

作者： Pick, Lauren Princeton University

学位级别：Ph.D., Doctor of Philosophy

Automated software verification techniques, while widely successful, often suffer from scalability issues due to state-space explosion. In both automated and manual verification, modular approaches help scale verification by breaking verification problems into several easier-to-solve subproblems. These subproblems often involve discovering suitable invariants that can be used to help derive a proof that the entire system meets the desired specification. In this dissertation, I describe work toward developing modular automatic techniques for software verification in which such invariants are discovered automatically. These techniques notably involve exploiting the structure and syntax of both system components and/or their specifications in order to find useful invariants for scaling verification. I have developed techniques for several related kinds of verification problems: the verification of k-safety properties, the verification of safety properties for general single-threaded interprocedural programs, and the verification of information-flow security—a specific kind of 2-safety property. For each of these verification problems, I have implemented the developed techniques in a verification tool and compared the tool to existing state-of-the-art tools for solving the verification problem. Experimental results demonstrate that the developed techniques help scale verification over existing state-of-the-art and allow more verification problems to be solved automatically.

关键词： Hyperproperty verification Invariant synthesis Modular verification software model checking software verification

来源：评论

学校读者我要写书评

暂无评论

Conditional Interpolation: Making Concurrent Program Verification More Effective 2021

Conditional Interpolation: Making Concurrent Program Verific...

引用

29th ACM Joint Meeting on European software Engineering Conference and Symposium on the Foundations of software Engineering (ESEC/FSE)

作者： Su, Jie Tian, Cong Duan, Zhenhua Xidian Univ ICTT & ISN Lab Xian Peoples R China

ISBN: (纸本)9781450385626

Due to the state-space explosion problem, efficient verification of real-world programs in large scale is still a big challenge. Particularly, thread alternation makes the verification of concurrent programs much more difficult since it aggravates this problem. In this paper, an application of Craig interpolation, namely conditional interpolation, is proposed to work together with CEGAR-based approach to reduce the state-space of concurrent tasks. Specifically, conditional interpolation is formalized to confine the reachable region of states so that infeasible conditional branches could be pruned. Furthermore, the generated conditional interpolants are utilized to shorten the interpolation paths, which makes the time consumed for verification significantly reduced. We have implemented the proposed approach on top of an open-source software model checker. Empirical results show that the conditional interpolation is effective in improving the verification efficiency of concurrent tasks.

关键词： software model checking concurrent program verification state-space reduction conditional interpolation CEGAR

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：