Talk:Formal equivalence checking
Latest comment: 12 years ago by Linas in topic SAT vs. ASP vs. SMT
| This is the talk page for discussing improvements to the Formal equivalence checking article. This is not a forum for general discussion of the article's subject. |
Article policies
|
| Find sources: Google (books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL |
 | This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | |||||||||||||||||
| ||||||||||||||||||
Software? edit
Is the conceptual equivalent for software, i.e. checking if any two well-defined programs that take N inputs and produce M outputs are equivalent, possible without simulating all of the possible input space? Wouter Lievens 09:39, 8 December 2006 (UTC)
- Yes, the problems are very similar, since you can turn the software into a state machine (that's what the combination of a compiler does, since a computer plus it's memory form a very large state machine.) Then, in theory, various forms of property checking could ensure they produce the same output. Note that the problem is even harder than combinatorial equivalence checking, since the outputs of the two programs may appear at different times, but it is possible and researchers are working on it. LouScheffer 14:38, 8 December 2006 (UTC)
- Added to article under 'generalizations'. LouScheffer 14:47, 8 December 2006 (UTC)
SAT vs. ASP vs. SMT edit
I'm exploring formal equivalence checking for the LLVM compiler, in order to implement superoptimization. Tom Crick's thesis uses answer set programming to describe the machine/instruction set; Sorav Bansal's peephole superoptimizer uses hand-rolled input to a SAT solver. Other folks in nearby areas use satisfiability modulo theories solvers. A discussion of which is "best" and why, would be a welcome addition to this article. linas (talk) 15:36, 14 June 2011 (UTC)