Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
详细信息    查看全文
文摘
We construct a correspondence between Horn clauses and finite tree automata (FTA). We construct a refined clauses from an FTA of the clauses and an infeasible trace. We propose a splitting operator on FTAs and describe its role in verification. We demonstrate the feasibility of our approach in practice.

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700