Optimization Modulo Theory (OMT) is an important extension of Satisfiability Modulo Theory (SMT), aiming to find models that satisfy constraints while optimizing objective functions. OMT naturally arises in program analysis and formal methods, making OMT solving an important and challenging task. OptiMathSAT is currently the state-of-the-art OMT solver supporting floating-point theories. It incrementally calls an SMT solver to prune the search space step by step until the optimal objective value is found. However, this frequent invocation of the SMT solver is highly inefficient. Therefore, this paper proposes a novel hybrid method consisting of two stages: coarse search and precise search. The coarse search stage quickly finds an approximate optimal model using an optimization search algorithm. The precise search stage then performs an SMT-based binary search starting from the approximate model to find the true optimal model (the OMT solution). Evidently, this hybrid approach reduces computational cost by rapidly shrinking the search space, thereby improving overall solving performance. We evaluated our method on benchmarks derived from SMT-LIB2 and real-world programs. Experimental results show that our method outperforms the current state-of-the-art in both effectiveness and efficiency.

The Message Passing Interface (MPI) is the standard programming model for high-performance computing, yet nondeterministic scheduling in concurrent executions makes reliability assurance highly challenging. Beyond deadlocks, property-related bugs such as modifying a send buffer before a nonblocking send completes or accessing a freed RMA window are often hard to reproduce and validate, as they typically manifest only under rare event interleavings and can be both latent and catastrophic. Existing dynamic checkers usually cover only the observed schedule of a single execution; dynamic verification largely focuses on deadlocks; and static techniques scale poorly to medium-to-large programs, often timing out or running out of memory. Overall, existing techniques do not support scalable analysis of temporal properties in large MPI programs. To address these limitations, we propose the first efficient predictive monitoring approach for temporal properties in MPI programs. From a single execution, we collect an event trace and use trace equivalence to predict the set of legal equivalent executions under the same input. We then check whether any predicted execution satisfies the target property. To make this process sound, we formalize three correctness criteria for MPI trace reordering and enforce them through MPI-semantics-driven dependency extraction, tracked with vector clocks. To improve efficiency, we exploit the bounded length of a pattern language and reduce long-trace reordering to reordering short patterns. We implement our approach in MPI-PRV, instantiate ten representative MPI bug properties, and evaluate it on 13 real-world MPI applications with 38 configurations. MPI-PRV successfully and correctly analyzes all 38 tasks, whereas MPI-SV and MUST analyze only 14 and 11 tasks, respectively. MPI-PRV also achieves orders-of-magnitude reductions in runtime and memory usage, demonstrating strong efficiency and scalability for large MPI programs.