pith. sign in

arxiv: 2507.11827 · v2 · submitted 2025-07-16 · 💻 cs.PL

Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation

Shaurya Gomber , Debangshu Banerjee , Gagandeep Singh This is my paper

Pith reviewed 2026-05-19 05:04 UTC · model grok-4.3

classification 💻 cs.PL
keywords abstract interpretationnumerical domainsevolving transformersgradient guidancepolyhedraprogram verificationadaptable analysisstatic analysis
0
0 comments X

The pith

An evolving abstract transformer searches a parametric space of sound invariants using gradient guidance to adapt across domains and balance precision with efficiency.

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

The paper aims to overcome the rigidity of traditional numerical abstract interpretation by introducing an evolving abstract transformer. Instead of fixed hand-crafted transformers, it uses a search over a parametric space of sound outputs. This is achieved through the Universal Parametric Output Space Encoder that builds the space for polyhedral domains and specific operators, and the Adaptive Gradient Guidance algorithm that searches it efficiently. Sympathetic readers would care because this enables reusing transformers across different domains and instructions, allows compositional reasoning, and lets users adjust the precision-efficiency tradeoff based on available runtime.

Core claim

The central claim is that the Evolving Abstract Transformer, implemented via UPOSE and AGG, works across domains and instructions, enables efficient precision-efficiency tradeoffs by adjusting the number of gradient steps, and reaches the most precise invariants up to 3.2x faster than existing baselines.

What carries the argument

The Universal Parametric Output Space Encoder (UPOSE), which builds a compact parametric space of sound outputs for any polyhedral numerical domain and any operator in the Quadratic-Bounded Guarded Operators class, allowing both individual instructions and structured sequences.

If this is right

  • Transformers become reusable across different numerical abstract domains such as Zones, Octagons, and Polyhedra.
  • Compositional reasoning over sequences of instructions is facilitated by the parametric space covering structured sequences.
  • Precision and efficiency can be traded off by varying the number of gradient steps in the search process.
  • The approach reaches the most precise invariants up to 3.2 times faster than current fixed transformer baselines.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Extending the parametric space beyond polyhedral domains could broaden the applicability to other abstract interpretation techniques.
  • Automating the discovery of new operators in the QGO class might further reduce manual engineering in program analysis.
  • Integration with existing static analysis tools could lead to more adaptive verification systems in practice.

Load-bearing premise

The Universal Parametric Output Space Encoder constructs a compact parametric space of sound outputs for any polyhedral numerical domain and any operator in the Quadratic-Bounded Guarded Operators class.

What would settle it

Demonstrating a polyhedral domain or QGO operator where the parametric space either misses some sound outputs or includes unsound ones would falsify the foundation of the evolving transformer.

Figures

Figures reproduced from arXiv: 2507.11827 by Debangshu Banerjee, Gagandeep Singh, Shaurya Gomber.

Figure 1
Figure 1. Figure 1: USTAD takes a numerical domain and an instruction sequence, and uses our synthesis algorithm to generate a parametric family of sound transformers for that sequence. It then uses this family of transformers to compute a family of sound outputs for the input abstract element, and applies a gradient-guided search, driven by user-specified parameters, to select a suitable output during analysis. precision or … view at source ↗
Figure 2
Figure 2. Figure 2: Examples demonstrating imprecision of current libraries for octagon analysis. [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Transformer output (blue) approaching the most-precise output (green) with increasing epochs [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: An example of instruction sequence merging in [PITH_FULL_IMAGE:figures/full_fig_p021_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Analysis results for the Zones domain with vs. without block merging. [PITH_FULL_IMAGE:figures/full_fig_p022_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Analysis results for the Octagon domain with vs. without block merging. [PITH_FULL_IMAGE:figures/full_fig_p023_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Analysis results for the Polyhedra domain with vs. without block merging (merging only blocks with [PITH_FULL_IMAGE:figures/full_fig_p023_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Invariant strengthening for Zones and Octagon domains with linear blocks only. Our method reaches [PITH_FULL_IMAGE:figures/full_fig_p024_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Runtime per transformer call vs. number of objectives and constraints. Our method scales more [PITH_FULL_IMAGE:figures/full_fig_p042_9.png] view at source ↗
read the original abstract

Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, causing three key limitations: transformers cannot be reused across domains; precise compositional reasoning over instruction sequences is difficult; and all downstream tasks must use the same fixed transformer regardless of precision or efficiency needs.To address this, we propose the Evolving Abstract Transformer, which replaces the fixed single-output design with an adaptable search over a parametric space of sound outputs via two algorithms. First, the Universal Parametric Output Space Encoder (UPOSE) constructs a compact parametric space of sound outputs for any polyhedral numerical domain and any operator in the Quadratic-Bounded Guarded Operators (QGO) class, covering both individual instructions and structured sequences. Second, the Adaptive Gradient Guidance (AGG) algorithm leverages the differentiable structure of UPOSE's output space to efficiently search it according to downstream objectives and available runtime, continually evolving the output as more time is provided. We implement these ideas in the AbsEvolve framework and evaluate across three numerical abstract domains: Zones, Octagons, and Polyhedra. Results show the evolving transformer works across domains and instructions, enables efficient precision-efficiency tradeoffs by adjusting number of gradient steps in the search, and reaches the most precise invariants up to 3.2x faster than existing baselines.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper claims that fixed hand-crafted abstract transformers in numerical abstract interpretation limit reuse across domains, compositional reasoning over sequences, and precision-efficiency tradeoffs. It introduces the Evolving Abstract Transformer via the Universal Parametric Output Space Encoder (UPOSE), which builds a compact parametric space of sound outputs for any polyhedral domain and any Quadratic-Bounded Guarded Operator (QGO) including sequences, and the Adaptive Gradient Guidance (AGG) algorithm, which uses differentiability to search this space efficiently. Implemented in AbsEvolve and evaluated on Zones, Octagons, and Polyhedra, the approach reportedly works across domains/instructions, supports runtime tradeoffs via gradient steps, and reaches precise invariants up to 3.2x faster than baselines.

Significance. If the UPOSE construction and soundness hold, the work could meaningfully advance abstract interpretation by reducing reliance on manual transformer design and enabling adaptable, reusable analyses with controllable precision/efficiency. The cross-domain empirical results and gradient-based search provide a concrete demonstration of practical benefits over static transformers.

major comments (1)
  1. [Abstract; §3 (UPOSE definition)] The central claim depends on UPOSE constructing a compact, sound parametric space for arbitrary polyhedral domains and the full QGO class (including structured sequences), yet the manuscript provides no explicit encoding mechanism, construction algorithm, or soundness argument for this representation. This directly affects the reusability, compositionality, and reported speedups.
minor comments (2)
  1. [Evaluation section] The evaluation lacks sufficient detail on exact baseline implementations, error bars, benchmark selection criteria, and runtime measurement methodology, which weakens verification of the 3.2x speedup and cross-domain claims.
  2. [§3 and §4] Notation for the parametric output space and gradient steps should be clarified with a small example or pseudocode to improve readability for readers unfamiliar with the QGO class.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their insightful review and recommendation for major revision. We address the primary concern about the UPOSE construction in detail below.

read point-by-point responses

  1. Referee: [Abstract; §3 (UPOSE definition)] The central claim depends on UPOSE constructing a compact, sound parametric space for arbitrary polyhedral domains and the full QGO class (including structured sequences), yet the manuscript provides no explicit encoding mechanism, construction algorithm, or soundness argument for this representation. This directly affects the reusability, compositionality, and reported speedups.

    Authors: We agree that a more explicit presentation of the UPOSE encoding mechanism, construction algorithm, and soundness argument would strengthen the paper. Section 3 introduces UPOSE as a parametric encoder that maps any polyhedral domain and QGO operator to a compact sound output space, but we will revise the manuscript to include a step-by-step construction algorithm and a dedicated soundness theorem with proof outline that applies to arbitrary polyhedral domains and sequences of operators. This revision will clarify how the approach enables reusability across domains and compositional reasoning over sequences, while supporting the reported performance benefits. revision: yes

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper introduces UPOSE as a construction of a parametric space for sound outputs over polyhedral domains and QGO operators, followed by AGG for gradient-guided search. The abstract and description frame these as algorithmic proposals grounded in abstract interpretation theory, without any quoted equations, fitted parameters renamed as predictions, or self-citations that bear the load of the central claims. The adaptability via number of gradient steps is presented as a runtime tradeoff rather than a reduction to inputs by definition. No load-bearing step reduces to self-definition or prior self-work by construction.

Axiom & Free-Parameter Ledger

1 free parameters · 1 axioms · 2 invented entities

The central claim rests on the soundness and compactness of the newly introduced UPOSE parametric space and the effectiveness of gradient search within it; these are supported by the proposed algorithms and empirical results rather than prior literature.

free parameters (1)
  • number of gradient steps
    Controls the precision-efficiency tradeoff during AGG search; chosen at runtime rather than fitted to data.
axioms (1)
  • domain assumption UPOSE produces only sound outputs for any polyhedral domain and QGO-class operator
    Invoked when constructing the parametric space; soundness is assumed to hold for the encoder design.
invented entities (2)
  • Universal Parametric Output Space Encoder (UPOSE) no independent evidence
    purpose: Constructs compact parametric space of sound outputs for domains and operators
    New component introduced to replace fixed transformers.
  • Adaptive Gradient Guidance (AGG) no independent evidence
    purpose: Searches the parametric space using differentiable structure and gradients
    New algorithm for adapting the transformer to objectives and runtime.

pith-pipeline@v0.9.0 · 5761 in / 1330 out tokens · 38109 ms · 2026-05-19T05:04:19.972620+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

55 extracted references · 55 canonical work pages

  1. [1]

    Roberto Bagnara, Patricia M Hill, and Enea Zaffanella. 2008. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming 72, 1-2 (2008), 3–21

    work page 2008

  2. [2]

    Maria-Florina Balcan, Travis Dick, Tuomas Sandholm, and Ellen Vitercik. 2018. Learning to Branch. In Proceedings of the 35th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 80) , Jennifer Dy and Andreas Krause (Eds.). PMLR, 344–353. https://proceedings.mlr.press/v80/balcan18a.html

    work page 2018

  3. [3]

    Mislav Balunović, Pavol Bielik, and Martin Vechev. 2018. Learning to solve SMT formulas. In Proceedings of the 32nd International Conference on Neural Information Processing Systems (Montréal, Canada) (NIPS’18). Curran Associates Inc., Red Hook, NY, USA, 10338–10349

    work page 2018

  4. [4]

    Debangshu Banerjee and Gagandeep Singh. 2024. Relational DNN verification with cross executional bound refinement. In Proceedings of the 41st International Conference on Machine Learning (Vienna, Austria) (ICML’24). JMLR.org, Article 111, 29 pages

    work page 2024

  5. [5]

    Debangshu Banerjee, Changming Xu, and Gagandeep Singh. 2024. Input-Relational Verification of Deep Neural Networks. Proc. ACM Program. Lang. 8, PLDI, Article 147 (June 2024), 27 pages. doi:10.1145/3656377

    work page doi:10.1145/3656377 2024

  6. [6]

    Bertsekas

    Dimitri P. Bertsekas. 1999. Nonlinear Programming (2nd ed.). Athena Scientific

    work page 1999

  7. [7]

    Dirk Beyer. 2016. Reliable and Reproducible Competition Results with BenchExec and Witnesses Report on SV-COMP

    work page 2016

  8. [8]

    Springer-Verlag, Berlin, Heidelberg, 887–904

    In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636. Springer-Verlag, Berlin, Heidelberg, 887–904. doi:10.1007/978-3-662-49674-9_55

    work page doi:10.1007/978-3-662-49674-9_55

  9. [9]

    Stephen Boyd and Lieven Vandenberghe. 2004. Convex Optimization. Cambridge University Press

    work page 2004

  10. [10]

    Aziem Chawdhary and Andy King. 2018. Closing the Performance Gap Between Doubles and Rationals for Octagons. In Static Analysis, Andreas Podelski (Ed.). Springer International Publishing, Cham, 187–204

    work page 2018

  11. [11]

    Aziem Chawdhary, Ed Robbins, and Andy King. 2019. Incrementally closing octagons. Formal Methods in System Design 54, 2 (2019), 232–277. doi:10.1007/s10703-017-0314-7

    work page doi:10.1007/s10703-017-0314-7 2019

  12. [12]

    Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InProceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California) (POPL ’77). Association for Computing Machinery, New York, NY, USA, 23...

    work page doi:10.1145/512950.512973 1977

  13. [13]

    Patrick Cousot and Radhia Cousot. 1977. Static determination of dynamic properties of generalized type unions. In Proceedings of an ACM Conference on Language Design for Reliable Software (Raleigh, North Carolina). Association for Computing Machinery, New York, NY, USA, 77–94. doi:10.1145/800022.808314

    work page doi:10.1145/800022.808314 1977

  14. [14]

    Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival

    work page

  15. [15]

    In Proceedings of the 14th European Conference on Programming Languages and Systems (Edinburgh, UK) (ESOP’05)

    The ASTREÉ analyzer. In Proceedings of the 14th European Conference on Programming Languages and Systems (Edinburgh, UK) (ESOP’05). Springer-Verlag, Berlin, Heidelberg, 21–30. doi:10.1007/978-3-540-31987-0_3

    work page doi:10.1007/978-3-540-31987-0_3

  16. [16]

    Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato. 2019. A 2I: abstract2interpretation. Proc. ACM Program. Lang. 3, POPL, Article 42 (Jan. 2019), 31 pages. doi:10.1145/3290355

    work page doi:10.1145/3290355 2019

  17. [18]

    Patrick Cousot and Nicolas Halbwachs. 1978. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Tucson, Arizona) (POPL ’78). Association for Computing Machinery, New York, NY, USA, 84–96. doi:10.1145/512760.512770

    work page doi:10.1145/512760.512770 1978

  18. [19]

    Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanović, and Martin Vechev. 2022. Complete Verification via Multi- Neuron Relaxation Guided Branch-and-Bound. In International Conference on Learning Representations . https:// openreview.net/forum?id=l_amHf1oaK

    work page 2022

  19. [20]

    Navas, Peter Schachte, Harald Søndergaard, and Peter J

    Graeme Gange, Zequn Ma, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2021. A Fresh Look at Zones and Octagons. ACM Trans. Program. Lang. Syst. 43, 3, Article 11 (Sept. 2021), 51 pages. doi:10.1145/3457885

    work page doi:10.1145/3457885 2021

  20. [21]

    Navas, Peter Schachte, Harald Søndergaard, and Peter J

    Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2016. Exploiting Sparsity in Difference-Bound Matrices. In Static Analysis, Xavier Rival (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 189–211

    work page 2016

  21. [22]

    Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A Navas. 2015. The SeaHorn verification framework. In International Conference on Computer Aided Verification . Springer, 343–361

    work page 2015

  22. [23]

    Gurobi Support. 2024. Non-Convex MIQP with Bilinear Terms. https://support.gurobi.com/hc/en-us/community/ posts/29050048200593/comments/29055912559889. Accessed April 2025

    work page arXiv 2024

  23. [24]

    Jingxuan He, Gagandeep Singh, Markus Püschel, and Martin Vechev. 2020. Learning fast and precise numerical analysis. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (London, UK) (PLDI 2020). Association for Computing Machinery, New York, NY, USA, 1112–1127. doi:10.1145/3385412.3386016 , Vol. 1, No. 1, Ar...

    work page doi:10.1145/3385412.3386016 2020

  24. [25]

    Kihong Heo, Hakjoo Oh, and Hongseok Yang. 2016. Learning a Variable-Clustering Strategy for Octagon from Labeled Data Generated by a Static Analysis. InStatic Analysis, Xavier Rival (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 237–256

    work page 2016

  25. [26]

    Kihong Heo, Hakjoo Oh, and Hongseok Yang. 2019. Resource-Aware Program Analysis Via Online Abstraction Coarsening. In 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE) . 94–104. doi:10.1109/ICSE. 2019.00027

    work page doi:10.1109/icse 2019

  26. [27]

    Bertrand Jeannet and Antoine Miné. 2009. Apron: A library of numerical abstract domains for static analysis. In International Conference on Computer Aided Verification . Springer, 661–667

    work page 2009

  27. [28]

    Jiahong Jiang, Liqian Chen, Xueguang Wu, and Ji Wang. 2017. Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT. In Verification, Model Checking, and Abstract Interpretation , Ahmed Bouajjani and David Monniaux (Eds.). Springer International Publishing, Cham, 310–329

    work page 2017

  28. [29]

    Jacques-Henri Jourdan. 2017. Sparsity Preserving Algorithms for Octagons. Electronic Notes in Theoretical Computer Science 331 (2017), 57–70. doi:10.1016/j.entcs.2017.02.004 Proceedings of the Sixth Workshop on Numerical and Symbolic Abstract Domains (NSAD 2016)

    work page doi:10.1016/j.entcs.2017.02.004 2017

  29. [30]

    Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D’Antoni, Thomas Reps, and Subhajit Roy. 2022. Synthesizing abstract transformers. Proc. ACM Program. Lang. 6, OOPSLA2, Article 171 (Oct. 2022), 29 pages. doi:10.1145/3563334

    work page doi:10.1145/3563334 2022

  30. [31]

    Pankaj Kumar Kalita, Thomas Reps, and Subhajit Roy. 2025. Synthesizing Abstract Transformers for Reduced-Product Domains. In Static Analysis, Roberto Giacobazzi and Alessandra Gorla (Eds.). Springer Nature Switzerland, Cham, 147–172

    work page 2025

  31. [32]

    Jacob Laurel, Siyuan Qian, Gagandeep Singh, and Sasa Misailovic. 2023. Synthesizing Precise Static Analyzers for Automatic Differentiation. Proceedings of the ACM on Programming Languages 7 (10 2023), 1964–1992. doi:10.1145/ 3622867

    work page 2023

  32. [33]

    Vincent Laviron and Francesco Logozzo. 2009. SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities. In Verification, Model Checking, and Abstract Interpretation , Neil D. Jones and Markus Müller-Olm (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 229–244

    work page 2009

  33. [34]

    Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, and Marsha Chechik. 2014. Symbolic optimization with SMT solvers. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, California, USA) (POPL ’14). Association for Computing Machinery, New York, NY, USA, 607–618. doi:10. 1145/2535838.2535857

    work page arXiv 2014

  34. [35]

    Francesco Logozzo and Manuel Fähndrich. 2008. Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In Proceedings of the 2008 ACM Symposium on Applied Computing (Fortaleza, Ceara, Brazil) (SAC ’08). Association for Computing Machinery, New York, NY, USA, 184–188. doi:10.1145/1363686.1363736

    work page doi:10.1145/1363686.1363736 2008

  35. [36]

    Francesco Logozzo and Manuel Fähndrich. 2008. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In Proceedings of the 2008 ACM symposium on Applied computing . 184–188

    work page 2008

  36. [37]

    Alexandre Maréchal, David Monniaux, and Michaël Périn. 2017. Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming. In Static Analysis, Francesco Ranzato (Ed.). Springer International Publishing, Cham, 212–231

    work page 2017

  37. [38]

    A. Mine. 2001. The octagon abstract domain. In Proceedings Eighth Working Conference on Reverse Engineering. 310–319. doi:10.1109/WCRE.2001.957836

    work page doi:10.1109/wcre.2001.957836 2001

  38. [39]

    Antoine Miné. 2002. A few graph-based relational numerical abstract domains. In International Static Analysis Symposium. Springer, 117–132

    work page 2002

  39. [40]

    Jorge Nocedal and Stephen J. Wright. 2006. Numerical Optimization (2nd ed.). Springer

    work page 2006

  40. [41]

    Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. 2014. Selective context-sensitivity guided by impact pre-analysis. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (Edinburgh, United Kingdom) (PLDI ’14). Association for Computing Machinery, New York, NY, USA, 475–484. doi:10.1145/2594...

    work page doi:10.1145/2594291.2594318 2014

  41. [42]

    Hakjoo Oh, Hongseok Yang, and Kwangkeun Yi. 2015. Learning a strategy for adapting a program analysis via bayesian optimisation. SIGPLAN Not. 50, 10 (Oct. 2015), 572–588. doi:10.1145/2858965.2814309

    work page doi:10.1145/2858965.2814309 2015

  42. [43]

    Brandon Paulsen and Chao Wang. 2022. LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions. In Tools and Algorithms for the Construction and Analysis of Systems , Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 357–376

    work page 2022

  43. [44]

    Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. 1999. Parametric shape analysis via 3-valued logic. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Antonio, Texas, USA) (POPL ’99). Association for Computing Machinery, New York, NY, USA, 105–118. doi:10.1145/292540.292552

    work page doi:10.1145/292540.292552 1999

  44. [45]

    Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna. 2005. Scalable analysis of linear systems using mathematical programming. In International Workshop on Verification, Model Checking, and Abstract Interpretation . Springer, 25–41. , Vol. 1, No. 1, Article . Publication date: September 2025. Universal Synthesis of Differentiably Tunable Numerical Abs...

    work page 2005

  45. [46]

    Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. A practical construction for decomposing numerical abstract domains. Proc. ACM Program. Lang. 2, POPL, Article 55 (Dec. 2017), 28 pages. doi:10.1145/3158143

    work page doi:10.1145/3158143 2017

  46. [47]

    Gagandeep Singh, Markus Püschel, and Martin Vechev. 2018. Fast Numerical Program Analysis with Reinforcement Learning. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 211–229

    work page 2018

  47. [48]

    Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2015. Making numerical program analysis fast. InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Stephen M. Blackburn (Eds.). ACM, 303–313

    work page 2015

  48. [49]

    Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2017. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 46–59

    work page 2017

  49. [50]

    Tarun Suresh, Debangshu Banerjee, and Gagandeep Singh. 2024. Relational Verification Leaps Forward with RABBit. In The Thirty-eighth Annual Conference on Neural Information Processing Systems . https://openreview.net/forum?id= W5U3XB1C11

    work page 2024

  50. [51]

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. InICML 2021 Workshop on Adversarial Machine Learning . https://openreview.net/forum?id=Mm3gxxTfT7A

    work page 2021

  51. [52]

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. 2021. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. InInternational Conference on Learning Representations . https://openreview.net/forum?id=nVZtXBI6LNn

    work page 2021

  52. [53]

    Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang. 2021. Program analysis via efficient symbolic abstraction. Proc. ACM Program. Lang. 5, OOPSLA, Article 118 (Oct. 2021), 32 pages. doi:10.1145/3485495

    work page doi:10.1145/3485495 2021

  53. [54]

    Hang Yu and David Monniaux. 2019. An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection. In Static Analysis: 26th International Symposium, SAS 2019, Porto, Portugal, October 8–11, 2019, Proceedings (Porto, Portugal). Springer-Verlag, Berlin, Heidelberg, 203–224. doi:10.1007/978-3-030-32304-2_11

    work page doi:10.1007/978-3-030-32304-2_11 2019

  54. [55]

    Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. 2014. On abstraction refinement for program analyses in Datalog. SIGPLAN Not. 49, 6 (June 2014), 239–248. doi:10.1145/2666356.2594327

    work page doi:10.1145/2666356.2594327 2014

  55. [56]

    Xin Zhang, Mayur Naik, and Hongseok Yang. 2013. Finding optimum abstractions in parametric dataflow analysis. SIGPLAN Not. 48, 6 (June 2013), 365–376. doi:10.1145/2499370.2462185 , Vol. 1, No. 1, Article . Publication date: September 2025. 30 Gomber et al. A DUALITY-BASED CONSTRUCTION OF SOUND PARAMETRIC SCALAR MAP Our algorithm to generate a parametric f...

    work page doi:10.1145/2499370.2462185 2013