A long time coming.....
Sometimes I find solutions to research questions to be very easy to find (e.g., we concieved and wrote up the paper "Proving thread termination" in perhaps 24 hours). This however was not the case for my new CAV paper "Proving conditional termination". You may find it simple now, but for some reason it took us years to develop this idea.
The research on this topic began as a conversation in 2006 between Mooly and I (in Tom Ball's office) after the first talk I gave at MSR-Redmond on Terminator. As visitors
to my lab came and went (e.g. Mooly, Sumit, Andrey, Tal) the thing snowballed into an ever growing ruckus carried out over visits and conference calls......co-authors would disagree and go off and write their own drafts, argue, plead, make alliances against each other, etc. It was terrifically fun, but I began to wonder if we'd ever find a workable solution. Finally, this winter, we got some traction and developed essentially what is in the paper today. After many many drafts, many failed starts, etc, the final version of the paper is finally done. Sigh.
Mooly is coming back to my lab this week.......I wonder what troublesome research question he'll propose this time ;-)
The research on this topic began as a conversation in 2006 between Mooly and I (in Tom Ball's office) after the first talk I gave at MSR-Redmond on Terminator. As visitors
to my lab came and went (e.g. Mooly, Sumit, Andrey, Tal) the thing snowballed into an ever growing ruckus carried out over visits and conference calls......co-authors would disagree and go off and write their own drafts, argue, plead, make alliances against each other, etc. It was terrifically fun, but I began to wonder if we'd ever find a workable solution. Finally, this winter, we got some traction and developed essentially what is in the paper today. After many many drafts, many failed starts, etc, the final version of the paper is finally done. Sigh.
Mooly is coming back to my lab this week.......I wonder what troublesome research question he'll propose this time ;-)
Proving conditional termination
Here are the slides from a talk on proving conditional termination that I gave at CMU.
CAV papers......
I co-authored a couple of papers that will appear at this year's CAV conference:
- Proving Conditional Termination, with Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv
- Scalable Shape Analysis for Systems Code, with the East London Massive
Subscribe to:
Posts (Atom)