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

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Prioritized Constraint-Aided Dynamic Partial-Order Reduction 22

Prioritized Constraint-Aided Dynamic Partial-Order Reduction

引用

Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering

作者： Jie Su Cong Tian Zuchao Yang Jiyu Yang Bin Yu Zhenhua Duan ICTT and ISN Laboratory Xidian University China

ISBN: (纸本)9781450394758

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

来源：评论

学校读者我要写书评

暂无评论

The Anchor Verifier for Blocking and Non-blocking concurrent Software

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2020年第OOPSLA期4卷 1–29页

作者： Flanagan, Cormac Freund, Stephen N. Univ Calif Santa Cruz Santa Cruz CA 95064 USA Williams Coll Williamstown MA 01267 USA

Verifying the correctness of concurrent software with subtle synchronization is notoriously challenging. We present the ANCHOR verifier, which is based on a new formalism for specifying synchronization disciplines that describes both (1) what memory accesses are permitted, and (2) how each permitted access commutes with concurrent operations of other threads (to facilitate reduction proofs). ANCHOR supports the verification of both lock-based blocking and cas-based non-blocking algorithms. Experiments on a variety concurrent data structures and algorithms show that ANCHOR significantly reduces the burden of concurrent verification.

关键词： concurrent program verification reduction synchronization

来源：评论

学校读者我要写书评

暂无评论

Scheduling Constraint Based Abstraction Refinement for Weak Memory Models 18

Scheduling Constraint Based Abstraction Refinement for Weak ...

引用

33rd IEEE/ACM International Conference on Automated Software Engineering (ASE)

作者： Yin, Liangze Dong, Wei Liu, Wanwei Wang, Ji Natl Univ Def Technol Lab Software Engn Complex Syst Changsha Hunan Peoples R China Natl Univ Def Technol State Key Lab High Performance Comp Changsha Hunan Peoples R China

ISBN: (纸本)9781450359375

Scheduling constraint based abstraction refinement (SCAR) is one of the most efficient methods for verifying programs under sequential consistency (SC). However, most multi-processor architectures implement weak memory models (WMMs) in order to improve the performance of a program. Due to the nondeterministic execution of those memory operations by the same thread, the behavior of a program under WMMs is much more complex than that under SC, which significantly increases the verification complexity. This paper elegantly extends the SCAR method to WMMs such as TSO and PSO. To capture the order requirements of an abstraction counterexample under WMMs, we have enriched the event order graph (EOG) of a counterexample such that it is competent for both SC and WMMs. We have also proposed a unified EOG generation method which can always obtain a minimal EOG efficiently. Experimental results on a large set of multi-threaded C programs show promising results of our method. It significantly outperforms state-of-the-art tools, and the time and memory it required to verify a program under TSO and PSO are roughly comparable to that under SC.

关键词： concurrent program verification weak memory model scheduling constraint event order graph

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：