Predator: a tool for verification of low-level list manipulation
TACAS'13 Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems（2013）
摘要
Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. This paper briefly introduces Predator and describes its participation in the Software Verification Competition SV-COMP'13 held at TACAS'13.
更多查看译文
关键词
Software Verification Competition SV-COMP,automated formal verification,core algorithm,higher-order list predicate,low-level memory manipulation,paper briefly,separation logic,sequential C program,system-level code,various form,low-level list manipulation
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要