TACAS11: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
2011-06-23 19:55
246 查看
Very interesting paper that combine AC(ssociativity and commutativity) operators with Shostak approach.
Generally, there are two approaches for theory combinations, nelson-oppen and Shostak.
The former one just pass equalities between T-solvers, so it is relativly easy to combine AC with it.
But for Shostak, it need to computer canonical form, which is not possible for AC.
Generally, there are two approaches for theory combinations, nelson-oppen and Shostak.
The former one just pass equalities between T-solvers, so it is relativly easy to combine AC with it.
But for Shostak, it need to computer canonical form, which is not possible for AC.
相关文章推荐
- TACAS11: Transition Invariants and Transition Predicate Abstraction for Program Termination
- Satisfiability Modulo Theories Competition (SMT-COMP)
- WHU1572---Cyy and Fzz (AC自动机+dp)
- 2017亚洲区域赛青岛赛区网络赛---1011题目(详细解答,AC)A Cubic number and A Cubic Number
- LTspice introduction - 5 Complex and AC analysis
- ACdream 1112 Alice and Bob (博弈&&素数筛选优化)
- Ground Estimation and Point Cloud Segmentation using SpatioTemporal Conditional Random Field(论文速读)
- TACAS11: Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
- php-url-rewriting-with-htaccess-and-microsoft-iis-url-rewriting
- 『Leetcode』All My AC Subjects and Solutions
- extract a crop from image and remark groundtruth(if left then flip)
- 多线程获取线程返回值---Future And CompletionService
- 【hdu - 1069 Monkey and Banana(动态规划,被坑死。一遍AC)】
- (.NET) IntelliSense difference of Extension Method name in Statement Completion for VB and C#.
- HDU 1028 Ignatius and the Princess III伊格和公主III(AC代码)母函数
- WIFI: N, Legacy and AC
- 多线程获取线程返回值---Future And CompletionService
- Reading table information for completion of table and column names You can turn off this feature to get a quicker startup with -
- Satisfiability Modulo Theories Competition (SMT-COMP)
- hdu 5566 Clarke and room(ac自动机+树链剖分)