This program is tentative and subject to change.
We present SYNVER - a novel, general purpose synthesizer for C programs with machine-checked proofs of their correctness using the Verified Software Toolchain framework. To do so, SYNVER employs two Large Language Models: the first is used to generate candidate programs from a user-provided specification, and the second helps to automatically generate proofs of correctness in the Rocq proof assistant. SYNVER ensures that generated programs adhere to a set of syntactic criteria that make candidate programs amenable to automated verification. To verify programs, SYNVER uses a novel proof generation strategy which combines a symbolic reasoning engine, specialized to reasoning about proof obligations generated by our verification framework, and a language model that handles obligations the symbolic engine cannot. We demonstrate the applicability of SYNVER using a diverse set of benchmarks drawn from the deductive program synthesis literature.
This program is tentative and subject to change.
Tue 18 NovDisplayed time zone: Seoul change
11:00 - 12:30 | |||
11:00 10mTalk | SMTgazer: Learning to Schedule SMT Algorithms via Bayesian Optimization Research Papers Chuan Luo Beihang University, Shaoke Cui Beihang University, Jianping Song Beihang University, Xindi Zhang State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China, Wei Wu Central South University; Xiangjiang Laboratory, Chanjuan Liu Dalian University of Technology, Shaowei Cai Institute of Software at Chinese Academy of Sciences, Chunming Hu Beihang University | ||
11:10 10mTalk | Efficient and Verifiable Proof Logging for MaxSAT Solving Research Papers | ||
11:20 10mTalk | Destabilizing Neurons to Generate Challenging Neural Network Verification Benchmarks Research Papers | ||
11:30 10mTalk | RELIA: Accelerating Analysis of Cloud Access Control Policies Research Papers Dan Wang Xi'an Jiaotong University, Peng Zhang Xi'an Jiaotong University, Zhenrong Gu Xi'an Jiaotong University, Weibo Lin Huawei Cloud, Shibiao Jiang Huawei Cloud, Zhu He Huawei Cloud, Xu Du Huawei Cloud, Longfei Chen Huawei Cloud, Jun Li Huawei, Xiaohong Guan Xi'an Jiaotong University | ||
11:40 10mTalk | Evolution-Aware Heuristics for GR(1) Realizability Checking Research Papers Dor Ma'ayan Tel Aviv University, Shahar Maoz Tel Aviv University, Jan Oliver Ringert Bauhaus-University Weimar | ||
11:50 10mTalk | Programmers’ Visual Attention on Function Call Graphs During Code Summarization Research Papers Samantha McLoughlin Vanderbilt University, Zachary Karas Vanderbilt University, Robert Wallace University of Notre Dame, Aakash Bansal Louisiana State University, Collin McMillan University of Notre Dame, Yu Huang Vanderbilt University | ||
12:00 10mTalk | LLM-Assisted Synthesis of High-Assurance C Programs Research Papers Prasita Mukherjee Purdue University, Minghai Lu Purdue University, Benjamin Delaware Purdue University Pre-print | ||
12:10 10mTalk | Faster Runtime Verification during Testing via Feedback-Guided Selective Monitoring Research Papers Shinhae Kim Cornell University, Saikat Dutta Cornell University, Owolabi Legunsen Cornell University | ||
12:20 10mTalk | Uncovering Discrimination Clusters: Quantifying and Explaining Systematic Fairness Violations Research Papers Ranit Debnath Akash University of Illinois Chicago, Ashish Kumar Pennsylvania State University, Verya Monjezi University of Texas at El Paso, Ashutosh Trivedi University of Colorado Boulder, Gang (Gary) Tan Pennsylvania State University, Saeid Tizpaz-Niari University of Illinois Chicago | ||