The Model-Constructing Satisfiability Calculus (MCSAT) framework has been applied to SMT problems over various arithmetic theories. NLSAT, an implementation using cylindrical algebraic decomposition (CAD) for explanation, is especially competitive for nonlinear real arithmetic (NRA) constraints. However, current Conflict-Driven Clause Learning (CDCL)-style algorithms only consider literal information when making decisions, and thus ignore the influence of clauses on arithmetic variables. This limitation may lead NLSAT to encounter unnecessary conflicts due to suboptimal literal choices. To address this issue, we analyze conflicts caused by literal decisions and incorporate clause-level information that directly affects arithmetic variables. We propose two main algorithmic improvements: a clause-level feasible-set-based look-ahead mechanism and an arithmetic propagation-based branching heuristic. We implement our solver, named clauseSMT, based on a dynamic variable ordering framework. Experiments indicate that clauseSMT is competitive on nonlinear real arithmetic problems compared with existing SMT solvers (CVC5, Z3, YICES2), and it outperforms all of them on satisfiable instances of SMT(QF_NRA) in SMT-LIB. We also evaluate the effectiveness of our proposed methods.
Mon 17 NovDisplayed time zone: Seoul change
14:00 - 15:30 | Formal Method & Verification 1Research Papers at Grand Hall 3 Chair(s): Nazareno Aguirre University of Rio Cuarto/CONICET, Argentina, and Guangdong Technion-Israel Institute of Technology, China | ||
14:00 10mTalk | ScaleCirc: Scaling the Analysis over Circom Circuits Research Papers Jinan Jiang The Hong Kong Polytechnic University, Haoran Qin The Hong Kong Polytechnic University, Xiapu Luo Hong Kong Polytechnic University | ||
14:10 10mTalk | Improving NLSAT for Nonlinear Real Arithmetic Research Papers Zhonghan Wang Institute of Software, Chinese Academy of Sciences Pre-print | ||
14:20 10mTalk | Bridging Natural Language and Formal Specification - Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs Research Papers Zhi Ma Xidian University, Cheng Wen Xidian University, Zhexin Su Xidian University, Xiao Liang Xidian University, Cong Tian Xidian University, Shengchao Qin Xidian University, Mengfei Yang China Academy of Space Technology Link to publication DOI Pre-print | ||
14:30 10mTalk | Diagnosing Performance Differences in Model Checkers via Runtime-Guided Problem Generation Research Papers Yibo Dong National University of Singapore, Yicong Xu East China Normal University, Wenjing Deng East China Normal University, Yu Chen Chuzhou University, Xiaoyu Zhang East China Normal University, Jianwen Li East China Normal University, China, Chengyu Zhang Loughborough University, Geguang Pu East China Normal University, China | ||
14:40 10mTalk | VERT: Polyglot Verified Equivalent Rust Transpilation with Large Language Models Research Papers Aidan Z.H. Yang Carnegie Mellon University, Yoshiki Takashima Yale Law School, Brandon Paulsen Amazon, Joey Dodds Amazon, Daniel Kroening Amazon | ||
14:50 10mTalk | Agentic Specification Generator for Move Programs Research Papers Yu-Fu Fu Georgia Institute of Technology, Meng Xu University of Waterloo, Taesoo Kim Georgia Institute of Technology Pre-print | ||
15:00 10mTalk | How Big is the Automaton? Certified Lower Bounds on the Size of Presburger DFAs Research Papers Nicolas Amat ONERA - The French Aerospace Lab, Pierre Ganty IMDEA Software Institute, Spain, Alessio Mansutti IMDEA Software Institute | ||
15:10 10mTalk | Non-termination Witnesses and their Validation Research Papers Zsófia Ádám Department of Measurement and Information Systems, Budapest University of Technology and Economics, Paulína Ayaziová Masaryk University, Czechia, Levente Bajczi Budapest University of Technology and Economics, Dirk Beyer LMU Munich, Marek Jankola LMU Munich, Marian Lingsch-Rosenfeld LMU Munich, Jan Strejcek Masaryk University Link to publication | ||
15:20 10mTalk | PAT-Agent: Autoformalization for Model Checking Research Papers Xinyue Zuo National University of Singapore, Yifan Zhang National University of Singapore, Hongshu Wang National University of Singapore, Yufan Cai National University of Singapore, Zhe Hou Griffith University, Jing Sun School of Computer Science, University of Auckland, Jin Song Dong National University of Singapore | ||
