Daniel Seidel, Janis Voigtländer
The video of the presentation can be downloaded at
http://www.iai.uni-bonn.de/~ds/Flops2010/GenCountEx_Flops2010.mp4 (207.8 MB).
Unfortunately, we could not manage very good quality of the slides in the video. But the slides are available separately under http://www.iai.uni-bonn.de/~ds/Flops2010/GenCountEx_Flops2010_slides.pdf.
If broadband is good enough, there is also a version of the video with (slightly) better quality: http://www.iai.uni-bonn.de/~ds/Flops2010/GenCountEx_Flops2010.mpg (843.8 MB).
If you got interested in the presented work, the conference paper you can find at http://www.iai.uni-bonn.de/~jv/paper.pdf, and a much more detailed technical report is located at http://www.iai.uni-bonn.de/~jv/TUD-FI09-05.pdf.
Subscribe to:
Post Comments (Atom)
@authors: Many thanks for your efforts in preparing the online presentation! (Please let us know if/when you are online by posting a ping message here.)
ReplyDelete@audience: Please post your questions and comments here.
Hi, I enjoyed your video talk.
ReplyDeleteI am not an expert on this topic, so this may
be a stupid question.
Is your algorithm complete, in the sense that if there is a counterexample, your algorithm can always find it?
Daniel: ping.
ReplyDeleteHi Naoki.
ReplyDeleteThanks for the question about completeness. It is not a stupid question at all. I did not tell this in the talk, but the slides online contain an extra slide stating the concrete results about completeness/correctness.
In fact, the implemented algorithm is correct but not complete.
We started, as presented in the talk, with an algorithm only generating terms that are very likely suitable for counterexample generation (the terms are at least only typable with *-annotated type variables). And we claim that this algorithm (we call it TermFind) is complete in the sense that if it finds no counterexample then there is none. The reasons for the claim are (1) by the rule system we started with and (2) by a "worst case"-search strategy introducing (harmful) _|_ wherever possible.
However, it showed that generating the additional information for a whole counterexample is not easy at all and sometimes even impossible. So we had to simplify the algorithm a bit to generate whole counterexamples. The problematic rule is also shown on an extra-slide from the presentation, not shown in the talk. The resulting algorithm (we call it ExFind) is not complete anymore.
But, we can clearly describe where the problems lie. In the technical report in section 6.3 this is discussed.