Talk:Formal equivalence checking
| 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)