The narration step in LLM-solver loops is vulnerable to prompt injection that inverts verified solver conclusions, and hardened prompts reduce but do not eliminate the risk under adaptive attacks.
hub
Z3: An Efficient SMT Solver
25 Pith papers cite this work, alongside 6,309 external citations. Polarity classification is still indexing.
25
Pith papers citing it
6,309
external citations · OpenAlex
hub tools
citation-role summary
method 2
dataset 1
citation-polarity summary
representative citing papers
A bisimulation-invariant synthesis framework for optimal predicate pushdown in fold-based UDFs produces correct transformations that speed up 150 real pipelines by 2.4x on average.
SuperDP refutes ε-DP via simultaneous synthesis of input pairs and witness functions using upper expectation supermartingales and lower expectation submartingales, delivering the first fully automated, sound, and semi-complete method applicable to both discrete and continuous stochastic mechanisms.
Neuroforger generates certified violation witnesses for smart contracts by representing specs as Solidity tests with abstract-type variables, using LLMs to instantiate them, and validating via type checking plus execution.
SCARA introduces a four-stage pipeline using state-aware verification and constrained synthesis to remediate vulnerabilities in source-unavailable industrial software, reporting 100% precision and 88.9% success on a 15-case benchmark.
Event-B Agent is an LLM agent that synthesizes, refines, and repairs Event-B formal models from natural language requirements via iterative verification feedback loops.
Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.
An SMT-based active learning algorithm learns minimal nondeterministic weighted automata over arbitrary semirings, with partial correctness proofs, a sufficient termination condition, and experiments showing smaller models and fewer queries than baselines.
Residual errors after repair in multi-turn constraint reasoning are 98-100% satisfiable drift rather than contradiction, shown via DRIFT-Bench evaluations on four models and methods.
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
In concurrent graph games with distributed private randomness, memoryless strategies decide threshold reachability (NP-hard) and almost-sure reachability is NP-complete; IRATL extends ATL for probability thresholds without shared randomness.
Dicey Games characterize optimal strategies and complexity for teams using pairwise or limited shared randomness, proving they can exceed 1/4 win probability in a 4-player matching-pennies game against an adversary.
ESBMC-PLC+ unifies support for all major IEC 61131-3 formats (ST, LD, SCL) in a single ESBMC backend with k-induction for unbounded safety proofs and extended function block semantics.
Unified LOLA framework combining runtime verification and model-based diagnosis for simultaneous online fault detection and localization, supporting time-invariant, transient, and nondeterministic cases.
Symbolic execution with speculative library preloading recovers 29.8% more CFG nodes and 26.5% more edges than static analysis alone, with 100% precision and recall on library detection across 16 synthetic obfuscated benchmarks.
An L#-inspired active learning algorithm learns minimal separating DFAs for disjoint languages when one exists and outperforms prior methods on random and industrial benchmarks.
RL training compute for logical reasoning follows a power law with horizon depth whose exponent rises with logical expressiveness, yielding better downstream transfer when models train on richer logics.
AutoRocq is an LLM agent that learns proofs on-the-fly by collaborating with the Rocq prover to verify programs on SV-COMP benchmarks and Linux kernel modules.
Framework using abstract grammar transformations, theory-based algorithms, and graph-inspired canonization to detect and explain (in-)equivalence of context-free grammars, evaluated on educational datasets.
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
A framework repairs CPS requirements in Simulink by leveraging system execution data and is evaluated as effective on six real-world case studies covering 12 requirements.
Zorya now analyzes gc-compiled Go binaries and detects seven of eleven real-world vulnerabilities at the binary level, including a silent integer overflow missed by other tools without an oracle.
Presents an SMT encoding to automatically prove polyhedral abstractions for Petri nets, complete for flat nets via Presburger reachability.
Case study shows that CHC transformations eliminating inductive data structures enable effective verification of partial correctness and arithmetic properties for several sorting algorithms using existing solvers.
citing papers explorer
-
Analyzing the Narration Gap in LLM-Solver Loops
The narration step in LLM-solver loops is vulnerable to prompt injection that inverts verified solver conclusions, and hardened prompts reduce but do not eliminate the risk under adaptive attacks.
-
Optimal Predicate Pushdown Synthesis
A bisimulation-invariant synthesis framework for optimal predicate pushdown in fold-based UDFs produces correct transformations that speed up 150 real pipelines by 2.4x on average.
-
SuperDP: Differential Privacy Refutation via Supermartingales
SuperDP refutes ε-DP via simultaneous synthesis of input pairs and witness functions using upper expectation supermartingales and lower expectation submartingales, delivering the first fully automated, sound, and semi-complete method applicable to both discrete and continuous stochastic mechanisms.
-
Neuroforger: certified violation witnesses for smart contracts verification via LLMs
Neuroforger generates certified violation witnesses for smart contracts by representing specs as Solidity tests with abstract-type variables, using LLMs to instantiate them, and validating via type checking plus execution.
-
SCARA: A Semantics-Constrained Autonomous Remediation Agent for Opaque Industrial Software Vulnerabilities
SCARA introduces a four-stage pipeline using state-aware verification and constrained synthesis to remediate vulnerabilities in source-unavailable industrial software, reporting 100% precision and 88.9% success on a 15-case benchmark.
-
Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair
Event-B Agent is an LLM agent that synthesizes, refines, and repairs Event-B formal models from natural language requirements via iterative verification feedback loops.
-
Caesar: A Deductive Verifier for Probabilistic Programs
Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.
-
SMT-Based Active Learning of Weighted Automata
An SMT-based active learning algorithm learns minimal nondeterministic weighted automata over arbitrary semirings, with partial correctness proofs, a sufficient termination condition, and experiments showing smaller models and fewer queries than baselines.
-
Residual Drift Dominates Contradiction in Multi-Turn Constraint Reasoning
Residual errors after repair in multi-turn constraint reasoning are 98-100% satisfiable drift rather than contradiction, shown via DRIFT-Bench evaluations on four models and methods.
-
Trace-Guided Synthesis of Effectful Test Generators
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
-
Randomise Alone, Reach as a Team
In concurrent graph games with distributed private randomness, memoryless strategies decide threshold reachability (NP-hard) and almost-sure reachability is NP-complete; IRATL extends ATL for probability thresholds without shared randomness.
-
Dicey Games: Shared Sources of Randomness in Distributed Systems
Dicey Games characterize optimal strategies and complexity for teams using pairwise or limited shared randomness, proving they can exceed 1/4 win probability in a 4-player matching-pennies game against an adversary.
-
ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor
ESBMC-PLC+ unifies support for all major IEC 61131-3 formats (ST, LD, SCL) in a single ESBMC backend with k-induction for unbounded safety proofs and extended function block semantics.
-
A Unified Framework for Runtime Verification and Model-Based Diagnosis in LOLA
Unified LOLA framework combining runtime verification and model-based diagnosis for simultaneous online fault detection and localization, supporting time-invariant, transient, and nondeterministic cases.
-
Control Flow Graph Recovery for Dynamically Loaded Code via Symbolic Library Resolution
Symbolic execution with speculative library preloading recovers 29.8% more CFG nodes and 26.5% more edges than static analysis alone, with 100% precision and recall on library detection across 16 synthetic obfuscated benchmarks.
-
An $L^{\#}$ Based Algorithm for Active Learning of Minimal Separating Automata
An L#-inspired active learning algorithm learns minimal separating DFAs for disjoint languages when one exists and outperforms prior methods on random and industrial benchmarks.
-
Can RL Teach Long-Horizon Reasoning to LLMs? Expressiveness Is Key
RL training compute for logical reasoning follows a power law with horizon depth whose exponent rises with logical expressiveness, yielding better downstream transfer when models train on richer logics.
-
Agentic Verification of Software Systems
AutoRocq is an LLM agent that learns proofs on-the-fly by collaborating with the Rocq prover to verify programs on SV-COMP benchmarks and Linux kernel modules.
-
Detecting and Explaining (In-)equivalence of Context-Free Grammars
Framework using abstract grammar transformations, theory-based algorithms, and graph-inspired canonization to detect and explain (in-)equivalence of context-free grammars, evaluated on educational datasets.
-
Reformalization of the Jordan Curve Theorem
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
-
Automated Repair of Requirements for Cyber-Physical Systems in Simulink Requirements Tables
A framework repairs CPS requirements in Simulink by leveraging system execution data and is evaluated as effective on six real-world case studies covering 12 requirements.
-
From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries
Zorya now analyzes gc-compiled Go binaries and detects seven of eleven real-world vulnerabilities at the binary level, including a silent integer overflow missed by other tools without an oracle.
-
On the Complexity of Proving Polyhedral Reductions
Presents an SMT encoding to automatically prove polyhedral abstractions for Petri nets, complete for flat nets via Presburger reachability.
-
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
Case study shows that CHC transformations eliminating inductive data structures enable effective verification of partial correctness and arithmetic properties for several sorting algorithms using existing solvers.
- Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code