Many software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Program verifiers, however, tend to be customized for individual languages. Verification by compiling to a common encoding requires supporting full language syntax and semantics which is prohibitive for modern languages. We present POLYVER, an alternative compositional approach to polyglot verification that bootstraps off-the-shelf language-specific verifiers with abstraction and synthesis. POLYVER uses contracts written in an intermediate language to abstract individual procedures in the system. Our verification approach uses language-specific verifiers (e.g., for C or Rust) to validate these contracts and the UCLID5 model checker for com- positionally verifying a temporal property on the overall system using the contracts. The intermediate language sidesteps the need for compiling implementation languages to a common encoding, a key obstacle with polyglot verification. Finally, POLYVER automates the generation of contracts using synthesis oracles such as large-language-models (LLMs). Overall POLYVER performs contract synthesis and verification in a counterexample-guided abstraction refinement and inductive synthesis (CEGIS-CEGAR) loop to verify the system-level property. We use POLYVER to verify programs in the Lingua Franca polyglot language. We are able to verify systems with C and Rust procedures, as well as C language fragments that were unsupported in previous work.

Top-k dominance (TKD) query is an extended query method of skyline query and top-k query, which reveals the top-k dominant individuals in an incomplete dataset by analyzing the dominance relationships between individuals and is a common decision tool in intelligent recommendation applications. This research proposes two parallel query algorithms based on Spark computing engine to address the shortcomings of the parallel top-k-dominated query algorithms for dynamic incomplete datasets. The designed model achieves good performance in terms of runtime performance compared to previous studies.

Stochastic Boolean Satisfiability (SSAT) is a powerful representation for the concise encoding of quantified decision problems with uncertainty. While it shares commonalities with quantified Boolean formula (QBF) satisfiability and has the same PSPACE-complete complexity, SSAT solving tends to be more challenging as it involves expensive model counting, a.k.a. Sharp-SAT. To date, SSAT solvers, especially those imposing no restrictions on quantification levels, remain much lacking. In this paper, we present a new SSAT solver based on the framework of clause selection and cube distribution previously proposed for QBF solving. With model counting integrated and learning techniques strengthened, our solver is general and effective. Experimental results demonstrate the overall superiority of the proposed algorithm in both solving performance and memory usage compared to the state-of-the-art solvers on a number of benchmark formulas.

Logic regression aims to find a Boolean model involving binary covariates that predicts the response of an unknown system. It has many important applications, e.g., in data analysis and system design. In the 2019 ICCAD CAD Contest, the challenge of learning a compact circuit representing a black-box input-output pattern generator in a high dimensional Boolean space is formulated as the logic regression problem. This paper presents our winning approach to the problem based on a decision-tree reasoning procedure assisted with a template based preprocessing. Our methods outperformed other contestants in the competition in both prediction accuracy and circuit size.