We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification.
['Sagar Chaki', 'Edmund M. Clarke', 'Joël Ouaknine', 'Natasha Sharygina', 'Nishant Sinha']
Concurrent software verification with states, events, and deadlocks