Data-Driven Template-Free Invariant Generation

Yuan Xia, Jyotirmoy V. Deshmukh, Mukund Raghothaman +1

Automatic verification of concurrent programs faces state explosion due to the exponential possible interleavings of its sequential components coupled with large or infinite state…