~/xizhe yin @ ucr
This work presents a principled solution to generalizing the incremental graph processing, such that queries, without their a priori knowledge, can also be evaluated incrementally. The solution centers around the concept of graph triangle inequalities, an idea inspired by the classical triangle inequality principle in the Euclidean space. Interestingly, we found that similar principles can also be derived for a spectrum of vertex-specific graph problems.
TLC (Temporal Logic of Components) is a temporal program logic that offers inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, transformations on the assertion language are defined that can lower the specification of a component to be used as a subcomponent. The stubborn link and the perfect link components are mechanically verified in Coq proof assistant.
In the past I was involved in projects in the areas of programming languages and software engineering that cross different domains: from distributed to shared memory systems; from software verification to high-performance graph processing. I plan to add more details to those interesting projects in the future.