Interpolation-based model checking (IMC) is an important technique in modern formal verification tools. In essence, it relies on an abstraction and refinement process to derive an adequate image approximation for the reachability analysis. However, previous IMC algorithms only offer fixed degrees of abstraction and thus may fail in the proofs if the abstraction is too coarse- or fine-grained. In this paper, we propose an adaptive interpolation-based model checking algorithm in which the degree of abstraction can be adjusted on demand. That is, during the proof process, we closely monitor the effectiveness of the interpolation-based over-approximated image computation and thus adjust the degree of abstraction for the best performance. The experimental results confirm that our flexible interpolation indeed leads to an adequate degree of abstraction as our IMC algorithm outperforms previous ones in various aspects.

Interpolation is an important and distinguished method popularly applied to recent synthesis and verification research topics. Existing approaches generate interpolants by analyzing unsatisfiability (UNSAT) proofs from satisfiable (SAT) solvers. Unfortunately, the interpolant is predestinedly determined by how the UNSAT proof is logged. This particularly weakens the abstraction of interpolation-based model checking procedure. In this paper, a new approach to generate a variety of functionally different interpolants using simulation and SAT solving is proposed. We further seamlessly integrated the novel interpolant generation algorithm into a reinterpreted interpolation-based model checking procedure. Moreover, spurious counterexamples from the model checker further guide the generation of interpolants to refute excessive refinements. As an extra benefit, proof logging is not required for SAT solvers. Experiments show promising results of our interpolation-based model checker NewITP on solving a large set of HWMCC benchmarks.

Interpolation is an important and distinguished method popularly applied to recent synthesis and verification research topics. Existing approaches generate interpolants by analysing unsatisfiability proofs from SAT solvers. Unfortunately, the interpolant is predestinedly determined by how the unsatisfiability proof is logged. This particularly weakens the abstraction of interpolation-based model checking procedure. In this paper, a new approach to generate a variety of functionally different interpolants using simulation and SAT solving is proposed. We further seamlessly integrated the novel interpolant generation algorithm into the reinterpreted interpolation-based model checking procedure. Moreover, spurious counterexamples from the model checker further guide the generation of interpolants to refute excessive refinements. As an extra benefit, proof logging is not required for SAT solvers. Experiments show promising results of our interpolation-based model checker NewITP on solving a large set of HWMCC benchmarks.

Single carrier frequency division multiple access (SC-FDMA) is applied as the transmission technology for the uplink traffic in LTE networks. The radio resource allocation is one of the most important issues to achieve effective wireless communication. Most researches focus on maximizing the system throughput of SC-FDMA under changing channel condition. However, users may require different quality of services (QoS) for different applications. This paper studies the radio resource allocation for QoS users in using localized SC-FDMA transmission. The proposed scheme is divided into the matching algorithm and the radio resource assignment algorithm. The Gale-Shapley algorithm is applied to find the optimal matching of resource block (RB) by considering the channel condition and the desired QoS of UE. The Recursive Maximum Expansion (RME) algorithm is modified in this paper to effectively assign radio resource for UEs with different bandwidth demands. The video streaming, VoIP, and FTP traffic types were adopted for simulations. Our results show that the proposed scheme achieves better QoS satisfaction than that without matching mechanism.