Concert/C: A Language for Distributed Programming
Joshua S. Auerbach, Arthur P. Goldberg, et al.
WTEC 1994
We propose a methodology for designing sound and complete proof systems for proving progress properties of parallel programs under various fairness assumptions. Our methodology begins with a branching time temporal logic formula (CTL*) formula that expresses progress under a fairness assumption. The next step obtains an equivalent fixpoint characterization of this CTL* formula in the μ-calculus. The final step uses the fixpoint characterizations to extract proof systems for proving progress under the fairness constraint. The methodology guarantees that the proof rules so obtained are sound and relatively complete in the sense of Cook.
Joshua S. Auerbach, Arthur P. Goldberg, et al.
WTEC 1994
Marc Stoecklin, Kapil Singh, et al.
IBM J. Res. Dev
E. Allen Emerson, Charanjit S. Jutla
SIAM Journal on Computing
Josyula R. Rao, Pankaj Rohatgi
USENIX Security 2000