Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
复制标题
系统构建和分析的工具和算法 - 第 21 届国际会议，TACAS 2015，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2015，英国伦敦，2015 年 4 月 11-18 日，会议记录
DOI：
10.1007/978-3-662-46681-0_45
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Nguyen T
中科院分区：
文献类型：
--
作者：
Nguyen T
我们描述了一种新的CSeq模块，用于动态创建线程的多线程C程序验证。该模块实现了Lazy-CSeq中实现的延迟序列化算法的变体。主要的新奇之处在于，我们现在支持无限数量的上下文切换并允许无限循环，而允许的线程数量仍然是有限的。这是通过修改的序列化转换和使用CPAcheck作为顺序验证后端来实现的。
We describe a new CSeq module for the verification of multi-threaded C programs with dynamic thread creation. This module implements a variation of thelazy sequentializationalgorithm implemented in Lazy-CSeq. The main novelty is that we now support an unbounded number of context switches and allow unbounded loops, while the number of allowed threads still remains bounded. This is achieved by a modified sequentialization transformation and the use of the CPAchecker as sequential verification backend.