Andrey Rybalchenko

Program verification as constraint solving (also for existential and universal CTL properties)