001 Formalization of security arXiv Paper Gilles Barthe Yesterday 002 Formalizing Flag Algebras in Lean arXiv Paper Gyeong-Won Jeong, Seonghun Park et al. 5 days ago 003 Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL arXiv Paper Shuqing Zhao 5 days ago 004 Compiler-Grounded Hierarchical Diagnosis for LLM-Based Triton Kernel Optimization arXiv Paper Dongjie Chen, Ping Zhao et al. 6 days ago 005 GLP: A Grassroots, Multiagent, Concurrent, Logic Programming Language for AI arXiv Paper Ehud Shapiro Jul 23 006 How Rules Represent Causal Knowledge: Causal Modeling with Probabilistic Logic Programming arXiv Paper Kilian Rueckschloss, Felix Weitkaemper Jul 23 007 Logic Programming Semantics for Causal Processes arXiv Paper Felix Weitkämper Jul 23 008 Relaxed activation analysis of dataflow networks - A clock calculus for machine learning and real-time scheduling arXiv Paper William Gaudelier, Albert Cohen et al. Jul 23 009 Decode-Time Grammars: Constrained LLM Generation over a Refinement Order of Grammar Fragments arXiv Paper Shuoming Zhang, Ruiyuan Xu et al. Jul 20 010 ETAS: An Effect-Typed Language for Agent Systems arXiv Paper Huiri Tan, Yikun Wang et al. Jul 20 011 The Duality of Information Flow: Reconciling Robust Downgrading with Non-Interference arXiv Paper Hemant Gouni, Frank Pfenning et al. Jul 20 012 Exact Network Surgery: Functional Invariance and Gradient Plasticity in Reactive Computational Graphs arXiv Paper Abdallah Khemais Jul 18 013 AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language arXiv Paper Qiyuan Xu, Joshua Ong Jun Leang et al. Jul 17 014 Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code arXiv Paper Niels Mundler-Sasahara, Hristo Venev et al. Jul 15 015 Quantize with Confidence? An Empirical Study of Quantization for Code Generation arXiv Paper Saima Afrin, MD Zahidul Haque et al. Jul 15 016 Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases arXiv Paper Marcus J. Min, Mike He et al. Jul 14 017 Compile, Then Page: Executable SOP Programs and a Capability-Gated Runtime for Procedural LLM Agents arXiv Paper Chenglin Yu, Lichao Yin et al. Jul 13 018 Imprompt: A Language Framework for Prompt Programming arXiv Paper Chentian Wu, Shengyuan Yang et al. Jul 13 019 GRID: Grammar-Railed Decoding for Enterprise SQL Generation arXiv Paper Mohsen Arjmandi Jul 11 020 Instruction Set and Language for Hypergraphs arXiv Paper Mario Pascual-González, Ezequiel López-Rubio Jul 11 021 Ceci n'est pas une pipe: AI systems as semantic abstractions arXiv Paper J. Alglave, P. Cousot Jul 10 022 Volition Elicitation: Operational Semantics for People and Their Machines arXiv Paper Ehud Shapiro Jul 10 023 TypeProbe: Recovering Type Representations from Hidden States of Pre-trained Code Models arXiv Paper Giulia Gorgone, Fausto Carcassi Jul 9 024 Workflow as Knowledge: Semantic Persistence for LLM-Mediated Workflows arXiv Paper Emanuele Quinto, C. Rozzi et al. Jul 9 025 Finding and Understanding Miscompilation Bugs in the Solidity Compiler arXiv Paper Bhargava Shastry Jul 8 026 GradInf: Gradient Estimation as Probabilistic Inference arXiv Paper Gaurav Arya, Mathieu Huot et al. Jul 8 027 Representation Robustness Under Executable Reasoning Constraints in Large Language Models for Mathematical Problem Solving arXiv Paper Sagnik Nath, E. A. Graf et al. Jul 8 028 REFORGE: A Method for Benchmarking LLMs' Reverse Engineering Capabilities in Decompiled Binary Function Naming arXiv Paper Nicolas Koller, Andreas u. Schmidt Jul 7 029 InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs arXiv Paper Guangyuan Wu, Weining Cao et al. Jul 6 030 Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading Pipelines arXiv Paper X. Fonseca Jul 6 031 PatchOptic for Shared-State LLM Workflows with Projected Views and Verified Structured Updates arXiv Paper Zhaoyu Bai, Jiaqin Cai Jul 6 032 SPL: Orchestrating Workflows with Declarative Deterministic-Probabilistic Composition arXiv Paper Wensheng Gong Jul 6 033 Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python arXiv Paper Akira Tanaka, Yusuke Kawamoto Jul 4 034 Composable Verification Pipelines for Multi-Agent Systems arXiv Paper Julian Alfredo Mendez, Andreas Brännström Jul 3 035 Differentiate the Evaluator, Not the Program: An Efficient Runtime Representation for Neuro-Symbolic Learning arXiv Paper Lucas Sheneman Jul 3 036 LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean arXiv Paper Simon Jeanteur, Lorenzo Veronese et al. Jul 3 037 ShannonProver: Towards Automating Formal Cryptographic Proofs arXiv Paper Yiping Ma, Yu-Lin Tsai et al. Jul 3 038 Fixed-Set Robustness in Programming by Example: Example Corruption and Semantic Partition Recovery arXiv Paper Yuan Si, Jialu Zhang Jul 1 039 LLVM-Bench: Benchmarking and Advancing Large Language Models for LLVM Compiler Issue Resolution arXiv Paper Zhao Tian, Yingquan Zhao et al. Jul 1 040 AlgoBench: Benchmarking Algorithmic Adaptation in Code Generation arXiv Paper Xinyuan Song, Z. Cai et al. Jun 30 041 Langshaw: Declarative Interaction Protocols Based on Sayso and Conflict arXiv Paper Munindar P. Singh, S. Christie et al. Jun 28 042 Symbolon: Symbolic Execution by Learning Code Transformation arXiv Paper Jie Zhu, Penghui Li et al. Jun 27 043 An Empirical Study of LLM-Generated Specifications for VeriFast arXiv Paper Wenzhui Fan, M. Tran et al. Jun 25 044 Compiler-Driven Approximation Tuning for Hyperdimensional Computing arXiv Paper Xavier Routh, Abdul Rafae Noor et al. Jun 25 045 Mostly Automatic Translation of Language Interpreters from C to Safe Rust arXiv Paper Bo Wang et al. Jun 25 046 Theory-Scale Auto-Formalization of Logics for Computer Science arXiv Paper Yuming Feng, Frederick Pu et al. Jun 25 047 Axon: A Synthesizing Superoptimizer for Tensor Programs arXiv Paper Akash Kothari, Shaowei Zhu et al. Jun 24 048 Information flow security on persistent memory arXiv Paper Graeme Smith Jun 24 049 ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor arXiv Paper Pierre V. Dantas, Lucas C. Cordeiro et al. Jun 22 050 CNnotator: LLM-Guided Memory Safety Annotation Synthesis arXiv Paper Twain Byrnes, Mike Dodds Jun 20 051 The Alignment Problem in Constrained Code Generation arXiv Paper Matteo Biagiola, Jahrim Gabriele Cesario et al. Jun 19 052 Multi-LCB: Extending LiveCodeBench to Multiple Programming Languages arXiv Paper Maria Ivanova, Pavel Zadorozhny et al. Jun 18 053 ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking arXiv Paper Pierre V. Dantas, Lucas C. Cordeiro et al. Jun 17 054 VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving arXiv Paper Manish Acharya, Zhenyu Liao et al. Jun 17 055 Bridging Functional Correctness and Runtime Efficiency Gaps in LLM-Based Code Translation arXiv Paper Longhui Zhang, Jiahao Wang et al. Jun 16 056 Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics arXiv Paper Xiyu Zhai, Xinyi Chen et al. Jun 16 057 When the Next Step Is Not One Step: Distribution-Aware Execution Modeling for Concurrent Go Programs arXiv Paper Kaviru Hapuarachchi Jun 16 058 PromptMN: Pseudo Prompting Language arXiv Paper Enkhzol Dovdon Jun 15 059 Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems arXiv Paper Sajjad Khan Jun 15 060 obliv-clang: Real-World Oblivious Programming in C++ arXiv Paper Yunqian Luo, Mingyu Gao Jun 15