3 citations · 3 across the 7 of their papers we have counts for
8 papers
Shared-Context Batched Satisfiability
Jiening Siow, Hanrui Zuo, Hanyun Jiang +2
Program analyzers often issue batches of SMT queries that share a large symbolic context and differ only in a small predicate. We formalize this recurring pattern as \emph{Shared-C…
Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang +2
Loop invariant synthesis remains a central and pivotal bottleneck in formal software verification. Recent LLM-based Neuro-Symbolic tools have achieved impressive solve rates. Howev…
Synthesizing Best Abstract Transformers via Parallel Bit-Vector Optimization
Weiqi Wang, Peisen Yao, Hanrui Zuo +3
Abstract interpretation provides a principled foundation for constructing sound static analyses through systematic abstraction. A central challenge is synthesizing the best abstrac…
ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
Muhammad A. A. Pirzada, Weiqi Wang, Yiannis Charalambous +2
Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by…
Beyond Accuracy: A Geometric Stability Analysis of Large Language Models in Chess Evaluation
Xidan Song, Weiqi Wang, Ruifeng Cao +1
The evaluation of Large Language Models (LLMs) in complex reasoning domains typically relies on performance alignment with ground-truth oracles. In the domain of chess, this standa…
Assisting Research Proposal Writing with Large Language Models: Evaluation and Refinement
Jing Ren, Weiqi Wang
Large language models (LLMs) like ChatGPT are increasingly used in academic writing, yet issues such as incorrect or fabricated references raise ethical concerns. Moreover, current…
Supporting Software Formal Verification with Large Language Models: An Experimental Study
Weiqi Wang, Marie Farrell, Lucas C. Cordeiro +1
Formal methods have been employed for requirements verification for a long time. However, it is difficult to automatically derive properties from natural language requirements. Spe…
Common 7B Language Models Already Possess Strong Math Capabilities
Chen Li, Weiqi Wang, Jingcheng Hu +5
Mathematical capabilities were previously believed to emerge in common language models only at a very large scale or require extensive math-related pre-training. This paper shows t…