search

mschlund / FPsolve

FPsolve: solver for polynomial equations over omega-continuous semirings
BSD 2-Clause "Simplified" License
11 stars 5 forks source link

Equivalence Testing in the Counting Semiring #13

Open mschlund opened 11 years ago

mschlund commented 11 years ago

Find suitable algorithms to test the (in)equivalence of two elements of the counting-SR (depends on the representation, of course).

It would also be fine to have an incomplete test (since the theoretical complexity of testing equivalence of e.g. SL-sets is very high)

mschlund commented 10 years ago

Is of course possible in theory (see paper by Ginsburg and Spanier), but have yet to implement this... no idea if anywhere near practical

pierreganty commented 10 years ago

Could you be more specific? I suspect the following result might help you: Ganty, Iosif, Konečný. Underapproximation of Procedure Summaries for Integer Programs (TACAS 13) and whose implementation Flata is available on github.

pierreganty commented 10 years ago

Also, an updated version of the TACAS results are available here