Pith. sign in

REVIEW 5 major objections 5 minor 60 references

Specification Generation for Neural Networks in Systems

T0 review · 5 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper proposes SpecTRA, which automatically generates interval-based behavioral specifications for neural networks from observations of the trusted reference algorithms they replace, and uses those specifications to verify and attack…

desk verdict A genuinely useful specification-mining framework with an overclaimed vulnerability result; the core method deserves peer review, but the 'unknown vulnerabilities' claim needs to be reined in. read the letter →

arxiv 2412.03028 v1 pith:5OD526BX submitted 2024-12-04 cs.AI cs.SYeess.SY

Isha Chaudhary , Shuyi Lin , Cheng Tan , Gagandeep Singh This is my paper · ORCID
classification cs.AIcs.SYeess.SY
keywords specificationgenerationneuralnetworkverificationreferencealgorithmsadaptivebitratestreamingcongestioncontrolintervalconstraintsdensity-basedclusteringtrustworthybehavior
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that traditional rule-based algorithms that neural networks replace can serve as proxies for correct behavior. It presents SpecTRA, which mines offline observations of such reference algorithms into compact interval-based specifications: if the network's input lands in a learned box, its output must be one of the outputs the references allow there. The authors test this on adaptive bitrate streaming and congestion control, where the learned specifications cover reference behaviors far better than existing hand-written specifications and match intuitive expectations, such as low bitrates when the buffer is nearly empty. Used for verification and adversarial search, the specifications reveal concrete failures in current models, including choosing the lowest bitrate with a healthy buffer and the highest bitrate with a nearly empty buffer.

What carries the argument

The central machinery is the interesting behavior region: a local input region where the union of outputs from all references is a strict subset of the output space, so the references together rule out at least one behavior. SpecTRA builds these regions from a static log by partitioning each input dimension into $p$ equal bins, discarding bins that do not contain enough observations from every reference, and keeping bins where the union of reference outputs is non-trivial. It then runs DBSCAN on the selected regions grouped by their output set, with the representation threshold encoded as a minimum cluster size. The tightest axis-aligned box bounding a cluster forms the precondition $\varphi_S$, and the union of that cluster's reference outputs forms the postcondition $\psi_S$, so specification generation reduces to a volume-minimizing clustering problem solvable without query access or source code.

What would settle it

Run both references on a dense grid of points covering each generated precondition and check whether every point's reference outputs are contained in that specification's postcondition; a single point inside a precondition whose reference output falls outside the allowed set would refute the claim that the specs encode reference behavior. A sharper version: hold out a deployment log from the same references and see whether the reported support and confidence drop sharply, which would show the training observations were not representative.

Watch

Extended reading notes

Core claim

The paper's central claim is that reference algorithms—hand-crafted, production-tested heuristics that a neural component replaces—are effective proxies for correct behavior, so their observed outputs can be automatically consolidated into formal specifications. SpecTRA casts specification generation as an optimization problem: minimize the total volume of interval preconditions while covering at least a threshold fraction of interesting behavior regions, keeping each specification's representation above a threshold, and allowing at most $\tau_{\max}$ outputs in its postcondition. It solves this approximately by partitioning each input dimension, keeping regions with enough observations from every reference, selecting regions where the combined reference outputs exclude at least one possible output, and density-clustering those regions; each cluster becomes an interval precondition mapped to the union of reference outputs. On Pensieve and Aurora the resulting specification sets score substantially higher support than the hand-written baseline while keeping high confidence, and complete verification plus targeted attacks show the state-of-the-art models violate the specifications.

Load-bearing premise

The load-bearing premise is that the observations used to build the specifications fairly represent all the behavior that matters; if some input region is sparsely or biasedly observed, the learned specs can silently omit or misstate what the references would do there.

Editorial extensions

If this is right

  • Any system where a neural network replaces a trusted rule-based algorithm can get an automated behavioral contract, as long as a log of reference observations is available.
  • The generated specifications can be fed directly to complete neural network verifiers; the paper shows that all tested Pensieve models violate at least one specification, indicating that strong average performance does not guarantee trustworthy edge behavior.
  • The specifications capture intermediate behaviors that manually designed specifications miss, so testing and verification can go beyond extreme corner cases.
  • Because the specifications are learned from deployment logs, they can be used to compare models: a network that satisfies them and performs well is better aligned with developer expectations than one that does not.
  • The same pipeline should transfer to other system tasks with discrete or discretizable action spaces, such as scheduling, indexing, or query optimization.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A stress test the paper does not run: deliberately remove a rare but safety-critical reference behavior from the observation log and see whether the mined specification silently drops it; the current threshold filtering has no way to flag such gaps.
  • Reference agreement is treated as trustworthy, but shared defects or outdated assumptions in the references would be inherited by the specifications; pairing SpecTRA with independently derived safety properties could catch that.
  • Because observations are static, the specifications could go stale if deployment conditions drift; a continual variant that refreshes the clusters as new logs arrive would turn them into an evolving behavioral contract.
  • For discretized continuous outputs, the sign-based discretization for Aurora discards magnitude information, so the same approach could be extended to predicates over output magnitudes or to continuous postconditions.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 5 minor

Summary. The paper proposes SpecTRA, a framework that automatically generates pre/postcondition specifications for neural networks in computer systems from offline observations of traditional reference algorithms. Given observations of one or more references, SpecTRA partitions the input space, identifies 'interesting behavior regions' where the reference outputs are non-trivial, clusters these regions with DBSCAN, and emits interval-based preconditions mapped to postconditions that are unions of the reference outputs observed in each cluster. The framework is demonstrated on two applications: adaptive bitrate streaming (Pensieve, with BB and MPC references) and congestion control (Aurora, with BBR and Cubic references). The paper evaluates specifications with support/confidence metrics on training and test observations, compares them with prior manual specifications, attempts complete verification with αβ-CROWN, and uses PGD to construct falsifying attacks on Pensieve. The central claims are that the generated specifications are correct and match intuition, and that they reveal previously unknown vulnerabilities in state-of-the-art neural network controllers.

Significance. SpecTRA addresses a timely and practically important problem: how to obtain usable correctness specifications for neural-network-based system components without manual, domain-expert design. The reference-as-proxy hypothesis is appealing, and the paper contributes a concrete formulation, an implemented algorithm with released code, and a useful comparison against prior manual specifications in two realistic applications. The use of a complete verifier (αβ-CROWN) and the public availability of the code are strengths; the paper also provides an ablation study over several hyperparameters. If the empirical validation were strengthened, the framework could be a valuable building block for verifying and testing learned system components. However, as submitted, the load-bearing empirical claims—especially the 'previously unknown vulnerabilities' and 'correct' specifications—are not fully supported by the evidence presented, for the reasons detailed in the major comments.

major comments (5)
  1. [§5.3.2 and §4.2] The claim that SpecTRA exposes 'previously unknown vulnerabilities' is not established because the attack inputs may lie in the overapproximated part of a precondition box, outside any observed reference region. In §4.2, preconditions are the tightest hyperrectangles bounding clusters of interesting behavior regions (Algorithm 1, lines 11–12), and postconditions are unions of reference outputs for those regions; the verifier and the PGD attack quantify over the entire box, including inputs for which the reference outputs are unknown. For the two attacks in §5.3.2, the paper reports only the output of the BB reference (1850 kbps for attack (a), 300 kbps for attack (b)), not the MPC reference, and does not show that the attack inputs are close to any observation used to build the specification. If, on the exact attack inputs, one of the references outputs the same extreme value, then the specification is not actually falsified. To support the vulnerability conclusion, the authors should run all references on the exact attack inputs and report their outputs, or demonstrate that the attack inputs lie within observed interesting behavior regions (e.g., by reporting distances to nearest observations).
  2. [§5.2.1, Table 1] The quantitative evaluation is circular to a significant degree. SpecTRA generates specifications from the training observations of the references (Section 4.1), and then §5.2.1 measures support and confidence of the specifications on those same training observations. High training support/confidence is expected by construction and provides no independent confirmation of correctness. The test-set metrics are a genuine out-of-sample generalization check, but they still measure conformance to the reference behaviors, not whether those behaviors are correct. Consequently, the abstract and §5.2's claim that the specifications 'show evidence of being correct' overstates what Table 1 supports. The authors should either temper the correctness claim or provide an external validation, for example by evaluating whether states satisfying the specifications lead to measurably better QoE or throughput in a simulator, or by soliciting structured domain-expert assessment of a sample of the generated preconditions and postconditions.
  3. [Algorithm 1, line 5, and Appendix C] The 'certain fraction of observations' used to define important input regions is not specified anywhere in the paper, and the DBSCAN radius r is not concretely defined. Algorithm 1's input list (line 1) omits this fraction, and the text in §4.2 says only that important regions have 'at least a certain fraction of the available observations for every reference.' Appendix D reports chosen values for τ_rep, p, and τ_max, but not for this threshold. Appendix C says r is 'the minimum radius that can ideally contain the minimum number of points, if densely packed,' which is not operational. Since this threshold and the clustering radius directly determine ΓX and therefore all generated specifications, their absence makes the experiments unreproducible and leaves open the possibility that the reported specification quality is sensitive to unstated settings. The authors should state the exact threshold, the value of r, and the procedure used to set r, and ideally include a sensitivity analysis for these parameters.
  4. [§5.1 and §5.2.2, Specification 2] The congestion-control specification is very weak and does not provide evidence of a meaningful trustworthiness property. Because Aurora's real-valued output is discretized by the sign function (§5.1), the postcondition of Specification 2, 'Change in Sending Rate ∈ {+, −}', merely forbids the output exactly zero. This makes the reported confidence of 1.0 for the Aurora models nearly tautological for models that rarely output a zero rate change, and it weakens the paper's claim that the CC specification is useful for exposing vulnerabilities: a spec that allows all non-zero rate changes cannot detect the known 'repeatedly decrease to the minimal rate' failure mode discussed in the Introduction. The authors should either use a finer-grained discretization that yields more restrictive postconditions, or explicitly discuss this limitation and why the sign-based specification is nevertheless informative.
  5. [§4.2, Algorithm 1 lines 14–15] The paper states that the coverage constraint is handled with a 'best-effort approach' because the search over output subsets may terminate before gτ_cov is reached. This means the returned specification set Ψ is not guaranteed to satisfy the constraint in the optimization problem (7). The paper should flag this more prominently as an approximation, and report, for each application, whether the coverage threshold was actually reached; otherwise a reader cannot know whether the generated specifications meet the formal requirement stated in Section 3.
minor comments (5)
  1. [Abstract and §1] The phrase 'Our specifications show evidence of being correct' in the abstract and 'the high quality of our specifications' in the Contributions would be more accurate if qualified as 'high consistency with reference observations on test data', given the circularity discussed in the major comments.
  2. [§4.1] The notation is confusing when X is used for both the full input space and a local input region (e.g., 'Let X be such an input region ...' and 'The reference Rj's output YX,j ⊆ Y'). Using different symbols, such as representing regions by R or B, would improve readability.
  3. [§5.3.2] The claim that 'similar attacks exist for other models too' for Pensieve small and mid is not evidenced; the section only shows attacks on Pensieve (big), and Table 2's falsification counts do not identify which specifications were falsified or by what margin. Reporting representative attacks for the other models, or at least the attacked specification indices, would strengthen the claim.
  4. [§5.2.1] The comparison with Eliyahu et al. (2021) uses the negation of their 'bad system states' specifications as an approximation of a good-state specification. This adaptation is reasonable but should be explicitly justified, since negating a temporal property is not generally equivalent to specifying the desired behavior of individual transitions.
  5. [Appendix D] The ablation study reports support and confidence on training observations only; reporting test-observation results would help assess whether the selected hyperparameters overfit the training traces.

Circularity Check

1 steps flagged · score 4.0 of 10

Partial circularity: SpecTRA's training-support/confidence 'correctness' evidence is entailed by its own clustering construction; test-set metrics and the vulnerability experiments still carry independent content.

  1. fitted input called prediction [Section 5.2.1 (Equations 8-9, Table 1) versus Section 4.2, Algorithm 1 (lines 9-12)]
    "To evaluate the quality of the specifications, we check them against the observations from the references over the training and testing environments for the neural models. We use the specification evaluation metrics of support and confidence ... These results indicate that our specifications correctly encode more of the trusted behaviors of the references over the relevant (training and testing) input distributions of the NNs than the existing specifications."

    Training confidence is forced by the same construction that creates the specifications. Algorithm 1 sets each postcondition to psi_Si = union over cluster regions R of Y_X, where Y_X is itself defined as the union of the observed reference outputs in that region. For any training observation lying in a clustered interesting region, R_j(x) is by definition in Y_X and hence in psi_S, so Equation (9) automatically returns confidence 1 for those points. The high training support/confidence rows of Table 1 therefore mostly report that the clustering objective (coverage and representation) was achieved, not an independent correctness test. The test-set rows are genuinely out-of-sample and do provide independent evidence, so this is partial rather than total circularity.

full rationale

SpecTRA's core derivation—turning offline reference observations into interval preconditions and output-set postconditions via partitioning, interesting-region filtering, and DBSCAN clustering—is not circular in itself. The optimization, thresholds, and clustering are stated explicitly, and the resulting specifications are a well-defined function of the observations. I found no load-bearing self-citation, no imported uniqueness theorem, and no ansatz smuggled in from the authors' prior work. The one concrete circular step is the in-sample quality evaluation: confidence on training observations is entailed by the definition of the postcondition as the union of reference outputs over the clustered regions, so those Table 1 rows are a fit diagnostic rather than evidence that the specs are 'correct.' The test-set support/confidence numbers are out-of-sample and do support the generalization claim, which is why the score is not higher. The paper itself acknowledges in Section 3 and Section 4.1 that interval and region overapproximation can exclude outputs for unobserved inputs x-hat not in gamma_x; this is a real caveat for the Section 5.3.2 'previously unknown vulnerabilities' claim, since a PGD attack input can lie inside the precondition box but outside the observed interesting regions, making a 'falsification' potentially an artifact. However, that is an external-validity and ground-truth-assumption limitation, not circularity: the specification is presented as a testable hypothesis derived from references, not as a theorem entailed by its inputs. Overall, the central vulnerability finding is independent of the fitted confidence numbers, so a moderate score of 4 is appropriate.

Assumptions & free parameters 7 free parameters · 7 assumptions · 0 invented entities

The central claim rests on the domain assumption that reference algorithms encode trustworthy behavior, plus several user-chosen thresholds and clustering parameters that are tuned on the training observations. No new physical entities are introduced.

free parameters (7)
  • tau_cov = 1.0
    Coverage threshold set to 1 in experiments to obtain maximum coverage; chosen by authors, not derived.
  • tau_rep = 0.01
    Representation threshold selected from ablation (Appendix D) to balance support and confidence.
  • tau_max = 5 (ABR), 2 (CC)
    Maximum postcondition output count selected from ablation for each application.
  • p (partitions per input dimension) = 100 (ABR), 50 (CC)
    Number of equally-sized bins per input dimension; chosen from ablation and affects overapproximation and runtime.
  • history length = 3 (ABR), 4 (CC)
    Number of past time steps used as input features; chosen by ablation following prior feature choices.
  • DBSCAN radius r = unspecified, set to minimum radius to contain min samples
    Clustering radius influences cluster shape and spec volume; the exact selection rule is under-specified.
  • important-region observation fraction = unspecified
    Algorithm 1 line 5 requires regions to have at least a certain fraction of observations per reference, but the fraction is never stated.
assumptions (7)
  • domain assumption Reference algorithms encode trustworthy and correct domain behavior and are valid proxies for NN correctness.
    This is the paper's core hypothesis, stated in the Abstract and Section 1; no independent proof is provided.
  • domain assumption Offline observations of references are representative of the deployment input distribution.
    Section 4.1 assumes only access to static observations; representative coverage is required for interesting-region identification.
  • domain assumption Interval-box preconditions and union-of-output postconditions are expressive enough to capture useful trustworthy behaviors.
    Section 3 restricts specifications to hyperrectangles; this is a simplicity choice that may miss complex dependencies.
  • domain assumption Input regions where references jointly exclude at least one output are the only interesting behaviors worth specifying.
    Definition 1 defines interesting behaviors this way; unselective regions are discarded, which may omit valid constraints.
  • domain assumption Sign-discretized output for Aurora preserves the behavior relevant to congestion control specifications.
    Section 5.1 maps continuous rate changes to plus, minus, and zero; the magnitude of change is ignored.
  • domain assumption DBSCAN clustering by input proximity yields semantically coherent behavior regions.
    Section 4.2 relies on density-based clustering to group interesting regions; this assumes behavioral similarity correlates with input proximity.
  • domain assumption Retrained Aurora models on Pantheon traces are representative of the original Aurora for the CC evaluation.
    Section 5.1 and Appendix B retrain Aurora to align with BBR and Cubic observations; the original model is also tested, but retraining may change behavior.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Specification Generation for Neural Networks in Systems." pith.science (2026). https://pith.science/paper/5OD526BX

@misc{pith2026241203028,
  author       = {Pith},
  title        = {Pith review of: Specification Generation for Neural Networks in Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5OD526BX}},
  note         = {Machine review of arXiv:2412.03028}
}
read the original abstract

Specifications - precise mathematical representations of correct domain-specific behaviors - are crucial to guarantee the trustworthiness of computer systems. With the increasing development of neural networks as computer system components, specifications gain more importance as they can be used to regulate the behaviors of these black-box models. Traditionally, specifications are designed by domain experts based on their intuition of correct behavior. However, this is labor-intensive and hence not a scalable approach as computer system applications diversify. We hypothesize that the traditional (aka reference) algorithms that neural networks replace for higher performance can act as effective proxies for correct behaviors of the models, when available. This is because they have been used and tested for long enough to encode several aspects of the trustworthy/correct behaviors in the underlying domain. Driven by our hypothesis, we develop a novel automated framework, SpecTRA to generate specifications for neural networks using references. We formulate specification generation as an optimization problem and solve it with observations of reference behaviors. SpecTRA clusters similar observations into compact specifications. We present specifications generated by SpecTRA for neural networks in adaptive bit rate and congestion control algorithms. Our specifications show evidence of being correct and matching intuition. Moreover, we use our specifications to show several unknown vulnerabilities of the SOTA models for computer systems.

Figures

Figures reproduced from arXiv: 2412.03028 by the authors.

Figure 1
Figure 1. (Overview of SpecTRA) Observations from all the references (a) are given as input to our specification generation [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Ablation study for hyperparameters affecting the specifications [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

60 extracted references · 38 canonical work pages

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  2. [2]

    Maximal specification synthesis

    Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel. Maximal specification synthesis. SIGPLAN Not., 51 0 (1): 0 789–801, January 2016. ISSN 0362-1340. doi:10.1145/2914770.2837628. URL https://doi.org/10.1145/2914770.2837628

    arXiv 2016

  3. [3]

    Glenn Ammons, Rastislav Bod\' k, and James R. Larus. Mining specifications. SIGPLAN Not., 37 0 (1): 0 4–16, January 2002. ISSN 0362-1340. doi:10.1145/565816.503275. URL https://doi.org/10.1145/565816.503275

    arXiv 2002

  4. [4]

    Madhusudan, Shambwaditya Saha, Shiyu Wang, and Tao Xie

    Angello Astorga, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, and Tao Xie. Learning stateful preconditions modulo a test generator. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, page 775–787, New York, NY, USA, 2019. Association for Computing Machinery. ISBN 9781450367127. doi:10.1145/3314...

    arXiv 2019

  5. [5]

    Madhusudan, and Tao Xie

    Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, and Tao Xie. Synthesizing contracts correct modulo a test generator. Proc. ACM Program. Lang., 5 0 (OOPSLA), oct 2021. doi:10.1145/3485481. URL https://doi.org/10.1145/3485481

    work page doi:10.1145/3485481 2021

  6. [6]

    Madhusudan, and Sayan Mitra

    Angello Astorga, Chiao Hsieh, P. Madhusudan, and Sayan Mitra. Perception contracts for safety of ml-enabled systems. Proc. ACM Program. Lang., 7 0 (OOPSLA2), October 2023. doi:10.1145/3622875. URL https://doi.org/10.1145/3622875

    doi:10.1145/3622875 2023

  7. [7]

    Synthesizing robust adversarial examples, 2018

    Anish Athalye, Logan Engstrom, Andrew Ilyas, and Kevin Kwok. Synthesizing robust adversarial examples, 2018. URL https://arxiv.org/abs/1707.07397

    arXiv 2018

  8. [8]

    Developing a predictive model of quality of experience for internet video

    Athula Balachandran, Vyas Sekar, Aditya Akella, Srinivasan Seshan, Ion Stoica, and Hui Zhang. Developing a predictive model of quality of experience for internet video. SIGCOMM Comput. Commun. Rev., 43 0 (4): 0 339–350, aug 2013. ISSN 0146-4833. doi:10.1145/2534169.2486025. URL https://doi.org/10.1145/2534169.2486025

    arXiv 2013

Show all 60 references
  1. [9]

    Certifying geometric robustness of neural networks

    Mislav Balunovic, Maximilian Baader, Gagandeep Singh, Timon Gehr, and Martin Vechev. Certifying geometric robustness of neural networks. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d Alch\' e -Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing...

    2019

  2. [10]

    The Satisfiability Modulo Theories Library (SMT-LIB)

    Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB) . www.SMT-LIB.org , 2016

    2016

  3. [11]

    Specification inference using context-free language reachability

    Osbert Bastani, Saswat Anand, and Alex Aiken. Specification inference using context-free language reachability. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, page 553–566, New York, NY, USA, 2015. Association f...

    2015

  4. [12]

    Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The fourth international verification of neural networks competition (vnn-comp 2023): Summary and results, 2023

    2023

  5. [13]

    Stephen Gunn, Soheil Hassas Yeganeh, and Van Jacobson

    Neal Cardwell, Yuchung Cheng, C. Stephen Gunn, Soheil Hassas Yeganeh, and Van Jacobson. Bbr: congestion-based congestion control. Commun. ACM, 60 0 (2): 0 58–66, jan 2017. ISSN 0001-0782. doi:10.1145/3009824. URL https://doi.org/10.1145/3009824

    2017 doi

  6. [14]

    Property-driven evaluation of rl-controllers in self-driving datacenters

    Arnav Chakravarthy, Nina Narodytska, Asmitha Rathis, Marius Vilcu, and Gagandeep Singh. Property-driven evaluation of rl-controllers in self-driving datacenters. 2022. URL https://api.semanticscholar.org/CorpusID:254568173

    2022

  7. [15]

    Comet: Neural cost model explanation framework

    Isha Chaudhary, Alex Renda, Charith Mendis, and Gagandeep Singh. Comet: Neural cost model explanation framework. In P. Gibbons, G. Pekhimenko, and C. De Sa, editors, Proceedings of Machine Learning and Systems, volume 6, pages 499--511, 2024. URL https://proceedings.mlsys.org/...

    2024

  8. [16]

    Z3: an efficient smt solver

    Leonardo De Moura and Nikolaj Bj rner. Z3: an efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, page 337–340, Berlin, Heidelberg, 2008. Springer-Verla...

    2008

  9. [17]

    Supporting standardization of neural networks verification with vnnlib and coconet

    Stefano Demarchi, Dario Guidotti, Luca Pulina, and Armando Tacchella. Supporting standardization of neural networks verification with vnnlib and coconet. 10 2023. doi:10.29007/5pdh

    2023 doi

  10. [18]

    The mnist database of handwritten digit images for machine learning research [best of the web]

    Li Deng. The mnist database of handwritten digit images for machine learning research [best of the web]. IEEE Signal Processing Magazine, 29 0 (6): 0 141--142, 2012. doi:10.1109/MSP.2012.2211477

    2012

  11. [19]

    PCC vivace: Online-Learning congestion control

    Mo Dong, Tong Meng, Doron Zarchy, Engin Arslan, Yossi Gilad, Brighten Godfrey, and Michael Schapira. PCC vivace: Online-Learning congestion control. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18), pages 343--356, Renton, WA, April 2018. USENI...

    2018

  12. [20]

    Verifying learning-augmented systems

    Tomer Eliyahu, Yafim Kazak, Guy Katz, and Michael Schapira. Verifying learning-augmented systems. In Proceedings of the 2021 ACM SIGCOMM 2021 Conference, 2021

    2021

  13. [21]

    Ernst, Jake Cockrell, William G

    Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin. Dynamically discovering likely program invariants to support program evolution. In Proceedings of the 21st International Conference on Software Engineering, ICSE '99, page 213–224, New York, NY, USA, 1999....

    1999

  14. [22]

    A density-based algorithm for discovering clusters in large spatial databases with noise

    Martin Ester, Hans-Peter Kriegel, J\" o rg Sander, and Xiaowei Xu. A density-based algorithm for discovering clusters in large spatial databases with noise. In Proceedings of the Second International Conference on Knowledge Discovery and Data Mining, KDD'96, page 226–231. AAAI...

    1996

  15. [23]

    Robust physical-world attacks on deep learning models, 2018

    Kevin Eykholt, Ivan Evtimov, Earlence Fernandes, Bo Li, Amir Rahmati, Chaowei Xiao, Atul Prakash, Tadayoshi Kohno, and Dawn Song. Robust physical-world attacks on deep learning models, 2018. URL https://arxiv.org/abs/1707.08945

    2018 arXiv

  16. [24]

    Complete verification via multi-neuron relaxation guided branch-and-bound

    Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanovi \'c , and Martin Vechev. Complete verification via multi-neuron relaxation guided branch-and-bound. In International Conference on Learning Representations, 2022

    2022

  17. [25]

    Ai2: Safety and robustness certification of neural networks with abstract interpretation

    Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), pages 3--18, 2018. doi:10.1109/S...

    2018

  18. [26]

    Towards reliable neural specifications

    Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, and Xujie Si. Towards reliable neural specifications. In International Conference on Machine Learning, pages 11196--11212. PMLR, 2023

    2023

  19. [27]

    Learning minimal nap specifications for neural network verification

    Chuqin Geng, Zhaoyue Wang, Haolin Ye, Saifei Liao, and Xujie Si. Learning minimal nap specifications for neural network verification. arXiv preprint arXiv:2404.04662, 2024

    2024 arXiv

  20. [28]

    Cubic: a new tcp-friendly high-speed tcp variant

    Sangtae Ha, Injong Rhee, and Lisong Xu. Cubic: a new tcp-friendly high-speed tcp variant. ACM SIGOPS operating systems review, 42 0 (5): 0 64--74, 2008

    2008

  21. [29]

    Data Mining: Concepts and Techniques

    Jiawei Han, Micheline Kamber, and Jian Pei. Data Mining: Concepts and Techniques. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 3rd edition, 2011. ISBN 0123814790

    2011

  22. [30]

    Characterizing neural network verification for systems with NN4SysBench

    Haoyu He, Tianhao Wei, Huan Zhang, Changliu Liu, and Cheng Tan. Characterizing neural network verification for systems with NN4SysBench . In Workshop on Formal Verification of Machine Learning. ICML, 2022

    2022

  23. [31]

    C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12 0 (10): 0 576–580, oct 1969

    1969

  24. [32]

    A buffer-based approach to rate adaptation: Evidence from a large video streaming service

    Te-Yuan Huang, Ramesh Johari, Nick McKeown, Matthew Trunnell, and Mark Watson. A buffer-based approach to rate adaptation: Evidence from a large video streaming service. In Proceedings of the 2014 ACM conference on SIGCOMM, pages 187--198, 2014

    2014

  25. [33]

    Pawan Kumar

    Florian Jaeckle, Jingyue Lu, and M. Pawan Kumar. Neural network branch-and-bound for neural network verification, 2021. URL https://arxiv.org/abs/2107.12855

    2021 arXiv

  26. [34]

    A deep reinforcement learning perspective on internet congestion control

    Nathan Jay, Noga Rotman, Brighten Godfrey, Michael Schapira, and Aviv Tamar. A deep reinforcement learning perspective on internet congestion control. In International Conference on Machine Learning, pages 3050--3059. PMLR, 2019

    2019

  27. [35]

    When machine learning meets congestion control: A survey and comparison, 2020

    Huiling Jiang, Qing Li, Yong Jiang, Gengbiao Shen, Richard Sinnott, Chen Tian, and Mingwei Xu. When machine learning meets congestion control: A survey and comparison, 2020. URL https://arxiv.org/abs/2010.11397

    2020 arXiv

  28. [36]

    Reluplex: An efficient smt solver for verifying deep neural networks, 2017

    Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks, 2017. URL https://arxiv.org/abs/1702.01135

    2017 arXiv

  29. [37]

    Towards instance-optimized data systems

    Tim Kraska. Towards instance-optimized data systems. Proceedings of the VLDB Endowment, 14 0 (12), 2021

    2021

  30. [38]

    General ltl specification mining (t)

    Caroline Lemieux, Dennis Park, and Ivan Beschastnikh. General ltl specification mining (t). In 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 81--92, 2015. doi:10.1109/ASE.2015.71

    2015 doi

  31. [39]

    Exploring practical vulnerabilities of machine learning-based wireless systems

    Zikun Liu, Changming Xu, Emerson Sie, Gagandeep Singh, and Deepak Vasisht. Exploring practical vulnerabilities of machine learning-based wireless systems. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), pages 1801--1817, Boston, MA, April 202...

    2023

  32. [40]

    Towards deep learning models resistant to adversarial attacks, 2019

    Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks, 2019. URL https://arxiv.org/abs/1706.06083

    2019 arXiv

  33. [41]

    Neural adaptive video streaming with pensieve

    Hongzi Mao, Ravi Netravali, and Mohammad Alizadeh. Neural adaptive video streaming with pensieve. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, SIGCOMM '17, 2017

    2017

  34. [42]

    Learning scheduling algorithms for data processing clusters, 2019

    Hongzi Mao, Malte Schwarzkopf, Shaileshh Bojja Venkatakrishnan, Zili Meng, and Mohammad Alizadeh. Learning scheduling algorithms for data processing clusters, 2019. URL https://arxiv.org/abs/1810.01963

    2019 arXiv

  35. [43]

    Ithemal: Accurate, portable and fast basic block throughput estimation using deep neural networks, 2019

    Charith Mendis, Alex Renda, Saman Amarasinghe, and Michael Carbin. Ithemal: Accurate, portable and fast basic block throughput estimation using deep neural networks, 2019. URL https://arxiv.org/abs/1808.07412

    2019 arXiv

  36. [44]

    Interpreting deep learning-based networking systems

    Zili Meng, Minhu Wang, Jiasong Bai, Mingwei Xu, Hongzi Mao, and Hongxin Hu. Interpreting deep learning-based networking systems. In Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, an...

    2020

  37. [45]

    Robustness certification of generative models, 2020

    Matthew Mirman, Timon Gehr, and Martin Vechev. Robustness certification of generative models, 2020. URL https://arxiv.org/abs/2004.14756

    2020 arXiv

  38. [46]

    Synthesizing specifications, 2023

    Kanghee Park, Loris D'Antoni, and Thomas Reps. Synthesizing specifications, 2023

    2023

  39. [47]

    Adaptive bitrate selection: A survey

    Yusuf Sani, Andreas Mauthe, and Christopher Edwards. Adaptive bitrate selection: A survey. IEEE Communications Surveys & Tutorials, 19: 0 2985--3014, 2017. URL https://api.semanticscholar.org/CorpusID:10803927

    2017

  40. [48]

    Seshia, Ankush Desai, Tommaso Dreossi, Daniel J

    Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue. Formal specification for deep neural networks. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for ...

    2018

  41. [49]

    An abstract domain for certifying neural networks

    Gagandeep Singh, Timon Gehr, Markus P\" u schel, and Martin Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3 0 (POPL), January 2019. doi:10.1145/3290354. URL https://doi.org/10.1145/3290354

    2019 doi

  42. [50]

    Intriguing properties of neural networks, 2014

    Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks, 2014. URL https://arxiv.org/abs/1312.6199

    2014 arXiv

  43. [51]

    Building verified neural networks for computer systems with ouroboros

    Tianhao Wei, Zhihao Jia, Changliu Liu, and Cheng Tan. Building verified neural networks for computer systems with ouroboros. Proceedings of Machine Learning and Systems, 5, 2023

    2023

  44. [52]

    Enchanting program specification synthesis by large language models using static analysis and program verification, 2024

    Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. Enchanting program specification synthesis by large language models using static analysis and program verification, 2024. URL https://arxiv.org/abs/2404.00762

    2024 arXiv

  45. [53]

    Stochastic forecasts achieve high throughput and low delay over cellular networks

    Keith Winstein, Anirudh Sivaraman, and Hari Balakrishnan. Stochastic forecasts achieve high throughput and low delay over cellular networks. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13), pages 459--471, Lombard, IL, April 2013. USENIX Assoc...

    2013

  46. [54]

    Scalable verification of gnn-based job schedulers

    Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, and Gagandeep Singh. Scalable verification of gnn-based job schedulers. Proceedings of the ACM on Programming Languages, 6 0 (OOPSLA2): 0 1036--1065, 2022

    2022

  47. [55]

    Automatic perturbation analysis for scalable certified robustness and beyond

    Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33, 2020

    2020

  48. [56]

    Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers

    Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, and Bhavya Kailkhura. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. arXiv preprint arXiv:2011.13824, 2021

    2011 arXiv

  49. [57]

    Yan, Jestin Ma, Greg D

    Francis Y. Yan, Jestin Ma, Greg D. Hill, Deepti Raghavan, Riad S. Wahby, Philip Levis, and Keith Winstein. Pantheon: the training ground for internet congestion-control research. In 2018 USENIX Annual Technical Conference (USENIX ATC 18), pages 731--743, Boston, MA, July 2018....

    2018

  50. [58]

    Provable defense against geometric transformations

    Rem Yang, Jacob Laurel, Sasa Misailovic, and Gagandeep Singh. Provable defense against geometric transformations. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023 . OpenReview.net, 2023

    2023

  51. [59]

    A control-theoretic approach for dynamic adaptive video streaming over http

    Xiaoqi Yin, Abhishek Jindal, Vyas Sekar, and Bruno Sinopoli. A control-theoretic approach for dynamic adaptive video streaming over http. SIGCOMM Comput. Commun. Rev., 2015

    2015

  52. [60]

    G.P. Zhang. Neural networks for classification: a survey. IEEE Transactions on Systems, Man, and Cybernetics, Part C (Applications and Reviews), 30 0 (4): 0 451--462, 2000. doi:10.1109/5326.897072

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.