Accelerating IC3 Verification by Exploiting Unsatisfiable Cores and Satisfying ModelsAward Winner
This program is tentative and subject to change.
The IC3 algorithm represents a groundbreaking advancement in the field of model checking. However, its heavy reliance on numerous and frequent constraint-solving calls poses significant challenges when verifying complex programs. We observe that many of the constraints solved within IC3 share remarkable similarities. Based on this observation, we propose an IC3 acceleration verification method by reusing unsatisfiable cores and satisfying models of previous constraints. This method constructs an Unsatisfiable Core Library (UCL) and a Satisfying Model Library (SML) to store and index crucial unsatisfiable cores and satisfying models generated during the verification process. When a new constraint-solving request is received, our method preemptively determines the satisfiability of the constraint using the existing unsatisfiable cores and satisfying models. This approach can significantly reduce the number of required solver calls, thereby enhancing the verification efficiency. We have implemented our method on Kind2 and evaluated it on the standard benchmark suite of Kind2. Experimental evaluation demonstrates that, for those complex examples, our method can reduce the number of solver calls by an order of magnitude, and achieves a 4.35-fold speedup with even less memory consumption.
This program is tentative and subject to change.
Fri 17 AprDisplayed time zone: Brasilia, Distrito Federal, Brazil change
11:00 - 12:30 | Dependability and Security 9Research Track / Demonstrations / SE In Practice (SEIP) at Oceania VII Chair(s): Jieke Shi Singapore Management University | ||
11:00 15mTalk | Prophecy: Inferring Formal Properties from Neuron Activations Demonstrations Divya Gopinath KBR; NASA Ames, Corina S. Păsăreanu Carnegie Mellon University, Muhammad Usman University of Texas at Austin, USA File Attached | ||
11:15 15mTalk | Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification Research Track Paschal Amusuo Purdue University, Owen Cochell Michigan State University, Taylor Le Lievre Purdue University, Parth Vinod Patil Purdue University, Aravind Machiry Purdue University, James C. Davis Purdue University Pre-print | ||
11:30 15mTalk | Accurate Inference of Termination ConditionsAward Winner Research Track | ||
11:45 15mTalk | Verification of Multi-Model Stochastic Systems Research Track Radu Calinescu University of York, UK, Simos Gerasimou Cyprus University of Technology, Sinem Getir Yaman University of York, UK, Gricel Vázquez University of York, UK, Micah Bassett University of York, UK Pre-print | ||
12:00 15mTalk | Accelerating IC3 Verification by Exploiting Unsatisfiable Cores and Satisfying ModelsAward Winner Research Track Xinyi Gong National University of Defense Technology, Liangze Yin National University of Defense Technology, Yuhan Li National University of Defense Technology, Ke Kang National University of Defense Technology, Wei Dong National University of Defense Technology, Shanshan Li National University of Defense Technology, Ji Wang National University of Defense Technology | ||
12:15 15mTalk | Agentic Taxation Optimization via LLM SMT-Constraint Reasoning SE In Practice (SEIP) Ting Chien Hwang National Chengchi University, Fang Yu National Chengchi University, Jie-Hong Roland Jiang National Taiwan University | ||