arXiv subjects

Trey Woodlief

Publications and source records attributed to Trey Woodlief.

4 recordsLinked to original sources

arXiv2026

NeuroSTAR: Automata-guided Neuro-symbolic Specification Formalization

Automated translation of natural language (NL) descriptions into Linear Temporal Logic over finite traces (LTLf) is a prerequisite for automated formal verification of a system's dynamic behavior. Several LLM-based methods have recently shown potential for this task. However, they struggle with the nuance of natural language descriptions, which can lead LLMs to only partially capture the intended meaning. To address this limitation, we propose NeuroSTAR (Automata-guided Neuro-symbolic Specification Formalization), an NL-to-LTLf framework that builds on two insights. First, it leverages multiple generators to obtain diverse LTLf candidates. Second, it uses an automata-theoretic semantic comparison based on DFA traces to identify behavioral disagreements that guide formula refinement. We evaluate NeuroSTAR and show that it improves NL-to-LTLf translation performance by 8-18 percentage points relative to the prior state-of-the-art (SoTA) on unambiguous benchmarks. We further study its applicability to a body of driving law text, a complex, realistic, and reference-free domain critical for autonomous-vehicle specification. This study shows that NeuroSTAR can capture the necessary temporal semantics in 83.9% of the driving law sections, which demonstrates the effectiveness of automata-guided reference-free refinement in formalization.

cs.FL↗

arXiv2026

CoCoMUT: A Tool for Code-Context Mining and Automated Dataset Generation

Software-engineering assistants often need method-level context beyond an isolated body, including enclosing-class information, documentation, callers, callees, type hierarchy, and structural characteristics. Manually collecting this context is time-consuming, inconsistent, and difficult to reproduce across large Java projects. We present CoCoMUT, a Java tool for Code-Context Mining and Automated Dataset Generation. CoCoMUT extracts context for a focal method or generates datasets at class, package, or system scope. It discovers project structure, resolves build and classpath information, constructs a SootUp static call graph, and reconciles bytecode-level call edges with Spoon-based source extraction. Each method record combines source, class, documentation, call-graph, and metadata context, providing reproducible inputs for training and running learned software-engineering techniques. The key contribution is a reusable, task-independent pipeline that unifies build discovery, source extraction, call-graph construction, source-bytecode reconciliation, and versioned JSON dataset generation. The resulting records can be consumed individually as context for a focal method or collectively as datasets for documentation, explanation, testing, review, repair, search, and program-comprehension workflows. We evaluate CoCoMUT on 20 real-world Java repositories evenly split between Maven and Gradle. CoCoMUT processed all 20 repositories, emitting 56,512 method-context records and 386,048 serialized call edges. Among call edges whose bytecode targets belonged to project source, CoCoMUT reconciled 97.8% to source method identities. In a manual audit of 200 randomly sampled methods across 10 systems, 99.0% of generated context records passed all applicable correctness checks.

cs.SE↗

arXiv2026

STADA: Specification-based Testing for Autonomous Driving Agents

Simulation-based testing has become a standard approach to validating autonomous driving agents prior to real-world deployment. A high-quality validation campaign will exercise an agent in diverse contexts comprised of varying static environments, e.g., lanes, intersections, signage, and dynamic elements, e.g., vehicles and pedestrians. To achieve this, existing test generation techniques rely on template-based, manually constructed, or random scenario generation. When applied to validate formally specified safety requirements, such methods either require significant human effort or run the risk of missing important behavior related to the requirement. To address this gap, we present STADA, a Specification-based Test generation framework for Autonomous Driving Agents that systematically generates the space of scenarios defined by a formal specification expressed in temporal logic (LTLf). Given a specification, STADA constructs all distinct initial scenes, a diverse space of continuations of those scenes, and simulations that reflect the behaviors of the specification. Evaluation of STADA on a variety of LTLf specifications formalized in SCENEFLOW using three complementary coverage criteria demonstrates that STADA yields more than 2x higher coverage than the best baseline on the finest criteria and a 75% increase for the coarsest criteria. Moreover, it matches the coverage of the best baseline with 6 times fewer simulations. While set in the context of autonomous driving, the approach is applicable to other domains with rich simulation environments.

cs.SE↗

arXiv2019

Faster Biclique Mining in Near-Bipartite Graphs

Identifying dense bipartite subgraphs is a common graph data mining task. Many applications focus on the enumeration of all maximal bicliques (MBs), though sometimes the stricter variant of maximal induced bicliques (MIBs) is of interest. Recent work of Kloster et al. introduced a MIB-enumeration approach designed for "near-bipartite" graphs, where the runtime is parameterized by the size k of an odd cycle transversal (OCT), a vertex set whose deletion results in a bipartite graph. Their algorithm was shown to outperform the previously best known algorithm even when k was logarithmic in |V|. In this paper, we introduce two new algorithms optimized for near-bipartite graphs - one which enumerates MIBs in time O(M_I |V||E| k), and another based on the approach of Alexe et al. which enumerates MBs in time O(M_B |V||E| k), where M_I and M_B denote the number of MIBs and MBs in the graph, respectively. We implement all of our algorithms in open-source C++ code and experimentally verify that the OCT-based approaches are faster in practice than the previously existing algorithms on graphs with a wide variety of sizes, densities, and OCT decompositions.

cs.DS↗