Liming Cai

Sixiang Zhang, Aaron J. Yang, Liming Cai

RNA secondary structure is modeled with the novel arbitrary-order hidden Markov model (α-HMM). The α-HMM extends over the traditional HMM with capability to model stochastic events that may be in influenced by historically distant ones, making it suitable to account for long-range canonical base pairings between nucleotides, which constitute the RNA secondary structure. Unlike previous heavy-weight extensions over HMM, the α-HMM has the flexibility to apply restrictions on how one event may influence another in stochastic processes, enabling efficient prediction of RNA secondary structure including pseudoknots.

Fei He, Qianshan Yu, Liming Cai

Software systems evolve throughout their life cycles. Many revisions are produced over time. Model checking each revision of the software is impractical. Regression verification suggests reusing intermediate results from the previous verification runs. This paper proposes a fully automatic regression verification technique in the context of CEGAR. Procedure summaries, which describe the input/output behaviors of a procedure, are proposed as the intermediate results to be reused. Procedure summaries are reasonably small to store, technically easy to process, and do not require much extra computation effort to be reused. Reusing procedure summaries saves much analysis effort on the corresponding procedures. By combining regression verification and CEGAR, we propose a technique that is able to reuse procedure summaries across different abstract precisions and different program revisions. We performed extensive experiments on a large number of industrial programs (534 revisions of 89 Linux kernel device drivers). The results show that our approach can significantly improve the performance of regression verification.

Liang Ding, Di Chang, Russell Malmberg et al.

The seminal work of Chow and Liu (1968) shows that approximation of a finite probabilistic system by Markov trees can achieve the minimum information loss with the topology of a maximum spanning tree. Our current paper generalizes the result to Markov networks of tree width $\leq k$, for every fixed $k\geq 2$. In particular, we prove that approximation of a finite probabilistic system with such Markov networks has the minimum information loss when the network topology is achieved with a maximum spanning $k$-tree. While constructing a maximum spanning $k$-tree is intractable for even $k=2$, we show that polynomial algorithms can be ensured by a sufficient condition accommodated by many meaningful applications. In particular, we prove an efficient algorithm for learning the optimal topology of higher order correlations among random variables that belong to an underlying linear structure.