From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting
An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically valid if every finite execution path from any state in the first set to a terminating state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by a logically constrained term rewrite system to an all-path reachability problem of the system. In this paper, we extend the framework to verification of starvation freedom of asynchronous integer transition systems with shared variables such that some processes enter critical sections.
Tue 17 JanDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30
|Execution Time Program Verification With Tight Bounds|
|From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting|
PADLDOI File Attached
|Multiple Query Satisfiability of Constrained Horn Clauses|