Natural reductions for concurrent programs admit a sound-and-complete polynomial-time soundness check without synchronization but are coNP-hard under locking.
Title resolution pending
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
representative citing papers
Once4All synthesizes LLM-based generators from extracted SMT grammars and populates formula skeletons to fuzz Z3 and cvc5, discovering 43 confirmed bugs with 40 fixed.
LORIS detects local reasoning errors in LLM-generated proofs for loop invariants by translating natural-language steps to first-order logic implications and using invalid implications to refine the invariants, achieving 93.1% success on 460 C programs.
CODO automates comprehensive dataflow optimization on FPGAs, achieving 1.45x-4.52x speedups on kernels and up to 33.8x on DNN models over state-of-the-art frameworks.
SpecTune improves LLM-based automated program repair by deriving localized postconditions at execution checkpoints and using alpha and beta signals to produce precise fault-localization and patch-generation guidance.
AutoLALA automatically generates symbolic formulas for reuse distance and data movement complexity in affine loop programs using polyhedral lowering and Barvinok counting.
citing papers explorer
-
On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
Natural reductions for concurrent programs admit a sound-and-complete polynomial-time soundness check without synchronization but are coNP-hard under locking.
-
Once4All: Skeleton-Guided SMT Solver Fuzzing with LLM-Synthesized Generators
Once4All synthesizes LLM-based generators from extracted SMT grammars and populates formula skeletons to fuzz Z3 and cvc5, discovering 43 confirmed bugs with 40 fixed.
-
Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
LORIS detects local reasoning errors in LLM-generated proofs for loop invariants by translating natural-language steps to first-order logic implications and using invalid implications to refine the invariants, achieving 93.1% success on 460 C programs.
-
CODO: An Automated Compiler for Comprehensive Dataflow Optimization
CODO automates comprehensive dataflow optimization on FPGAs, achieving 1.45x-4.52x speedups on kernels and up to 33.8x on DNN models over state-of-the-art frameworks.
-
Enhancing Program Repair with Specification Guidance and Intermediate Behavioral Signals
SpecTune improves LLM-based automated program repair by deriving localized postconditions at execution checkpoints and using alpha and beta signals to produce precise fault-localization and patch-generation guidance.
-
AutoLALA: Automatic Loop Algebraic Locality Analysis for AI and HPC Kernels
AutoLALA automatically generates symbolic formulas for reuse distance and data movement complexity in affine loop programs using polyhedral lowering and Barvinok counting.