Sinfer: Inferring information flow lattices for checking self-stabilization

Self-stabilizing programs are guaranteed to recover from state corruption caused by software bugs or other events and eventually reach the correct state. Many real-world applications including embedded controllers and multimedia applications can be designed to make key components self-stabilizing. Type systems and static analyses can automatically check whether a program is self stabilizing. The existing approach for checking self-stabilization requires developers to manually annotate code. We present an annotation inference algorithm that automatically derives an initial set of annotations and therefore lowers the effort to build self-stabilizing systems. Our experience with the algorithm indicates that it effectively inferred annotations for our benchmarks.