Pith. sign in

REVIEW 4 major objections 6 minor 1 cited by

Neural Network Verification for Gliding Drone Control: A Case Study

T0 review · 4 major / 6 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read This paper shows that existing verification tools, combined with a new regression-specific adversarial-training method, can verify trajectory-adherence properties of an Alsomitra-inspired glider controller, yet the verified guarantees…

desk verdict A genuinely useful new benchmark case study with an unsupported headline claim about adversarial training; deserves peer review and a regression-matched control. read the letter →

arxiv 2505.00622 v1 pith:ASSDIXYW submitted 2025-05-01 cs.RO cs.AIcs.SYeess.SY

Colin Kessler , Ekaterina Komendantskaya , Marco Casadio , Ignazio Maria Viola , Thomas Flinkow , Albaraa Ammar Othman , Alistair Malhotra , Robbie McPherson This is my paper · ORCID
classification cs.ROcs.AIcs.SYeess.SY
keywords neuralnetworkverificationreachabilityanalysisadversarialtrainingregressioncontrolglidingmicrodroneAlsomitraLipschitzrobustnessclosed-loop
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 existing neural-network verification tools, combined with a new adversarial training scheme for regression networks, can verify safety-relevant properties of an Alsomitra-inspired gliding-drone controller, but only within a tightly constrained envelope. The drone is modelled as a falling plate with a displaced centre of mass, and the controller is a small ReLU network trained by behaviour cloning to follow a linear trajectory. The authors reduce an ideal infinite-horizon specification to five static properties checked with one verifier and a finite-horizon reachability property checked with another. Their central positive result is that adversarially trained controllers satisfy the first global property with $y^* = 30$ instead of $y^* = 46$, and reach the goal corridor after 20 seconds when the naive controller does not, while the verified guarantees remain too coarse for practical use.

What carries the argument

The load-bearing object is the quasi-steady aerodynamic model of a falling plate with a displaced centre of mass, taken from the literature and simplified for tractability by replacing $\tan\alpha$ with $x_2/x_1$ and constraining the pitch angle so that reachability computations can run. The second mechanism is the closed-loop controller: a $6\times 6 \times 4 \times 1$ ReLU network, trained on PID-generated regression data, whose single output actuates the centre-of-mass displacement. The third mechanism is adversarial training for regression: PGD with an RMSE loss augmented by a dynamically computed Lipschitz penalty that penalises large output-to-input gradient ratios. The argument is carried by pairing these trained networks with two verification pipelines: relational, regression-oriented properties in Vehicle/Marabou, and zonotope-based reachability in CORA, where a zonotope is a convex set representation that over-approximates all states reachable under the dynamics.

What would settle it

Compare the verified envelopes against wind-tunnel or free-flight measurements of an Alsomitra-inspired glider using the same controller: record the actual deviation from the target trajectory $x_6 = -x_5$ over 20 seconds. If real trajectories exceed the verified $y^*$ values or fail to reach the CORA goal region from the initial set $x_1=1, x_2=0, x_3=0, x_4=0, x_5=0, x_6\in[1.43,4.29]$, then the claim that these properties apply to the physical drone is falsified; a cheaper check is to integrate the full unsimplified dynamics model and compare against the simplified equations used for verification.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that this class of benchmarks — continuous regression control with complex nonlinear dynamics — is not yet directly verifiable, but a pragmatic pipeline can be assembled from existing tools. The ideal property, that the drone always stays within distance $y^*$ of the target line $x_6 = -x_5$ after some time, is split into two tasks: Vehicle/Marabou checks that the controller never commands a large deviation under relational constraints on the input state, and CORA checks that all trajectories from a small initial interval reach a goal region around the line within 20 seconds. Adversarial training using projected gradient descent with an RMSE loss augmented by a Lipschitz penalty yields networks that pass stricter versions of those properties than naively trained networks. The authors are explicit that the verified $y^*$ values are too large and the reachable initial sets too small for the guarantees to be immediately useful; the contribution is the first end-to-end demonstration that the tools can be adapted to this problem class, plus a catalogue of what must change.

Load-bearing premise

The verification results concern the simplified quasi-steady aerodynamic equations, so if those equations do not faithfully represent a real Alsomitra-inspired drone — and no wind-tunnel or field validation is given — every verified property is only about a simulation rather than the drone.

Editorial extensions

If this is right

  • Verifying a continuous regression controller in practice today means splitting the ideal property: static relational checks on the network plus finite-horizon reachability on the closed loop.
  • Adversarial training with a Lipschitz penalty improves the verification outcome on the first trajectory-adherence property, with $y^*$ dropping from 46 to 30, and lets the adversarial controller reach the goal corridor in 20 seconds where the naive controller does not.
  • The guarantees obtained are not yet deployment-grade: the verified $y^*$ values are large and the reachable initial sets are zero-width in five dimensions, so this is a proof of principle rather than a certification.
  • Tool development priorities follow directly from the case study: native input normalisation, relational properties that name multiple network outputs, support for multiple network calls, and cheaper Jacobian and Hessian approximations for reachability.
  • Regression-focused robustness training generalises the usual classification-oriented property-driven training, so the same scheme can be applied to other regression control tasks with nonlinear closed-loop dynamics.

Reading between the lines

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

  • Editorial inference: the regression adversarial-training scheme is plant-agnostic and should transfer directly to other passively falling or gliding microflyers, such as dandelion-inspired designs, provided their dynamics can be written as a tractable model.
  • Editorial inference: a sharper test of the robustness claim would compare naive and adversarial networks matched on regression accuracy ($R^2$), since the paper notes the reachability gap could partly reflect regression performance rather than robustness alone.
  • Editorial inference: if validation data ever confirm the simplified aerodynamics, the same pipeline would turn these coarse envelopes into flight-relevant guarantees; until then, the paper's transferable contribution is the catalogue of tool gaps: normalisation, relational properties, multi-network queries, and derivative complexity.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper presents a verification case study for a centimetre-scale Alsomitra-inspired gliding drone controlled by a neural network. The authors formulate an ideal safety/adherence property (following a linear target trajectory), then distill it into properties expressible in Vehicle/Marabou and CORA. They propose a regression adaptation of PGD-based adversarial training with a dynamic Lipschitz penalty, and compare a 'naive' network with an adversarially trained network and with property-driven-trained networks from a companion paper. The reported results are mixed: one global property improves under adversarial training (Property 1, y* from 46 to 30), another is unchanged, one fails for all networks, one is trivially easy, and a local robustness property is evaluated only on training data. The CORA reachability experiment shows the adversarial network reaching the goal region while the naive network does not. The paper concludes that a combination of existing tools and the proposed training methods could support this class of benchmarks once tool limitations are overcome.

Significance. If the claims are sustained, the paper provides a useful first end-to-end verification benchmark for a regression-controlled bio-inspired glider, with transferable lessons about normalization, relational properties, and reachability set explosion. The paper is commendably candid about tool shortcomings and about its own limitations, and the public release of verification artifacts is a strength. The main empirical claim about adversarial training improving performance and robustness is, however, not established by the data as presented: the comparison is confounded by differences in regression quality, and the local robustness property is evaluated on training data. The case-study and tool-integration contributions are worthwhile, but the central empirical conclusion needs either re-supporting or substantial weakening.

major comments (4)
  1. [Sects. 7.3, 8.2, 9.1; Tables 1-2, Fig. 7] The central comparison between the naive and adversarially trained networks is not matched on regression quality. Section 9.1 explicitly concedes that 'A better comparison could be made using NNs with equivalent regression performance on a test set of data, using a coefficient such as R2.' The reported improvements — Property 1 y* from 46 to 30 in Table 1 and the CORA reachability success in Fig. 7 — are therefore compatible with the alternative explanation that the adversarial network is simply a better regressor on the training distribution. This is load-bearing because the abstract states that the investigated training methods improve performance and robustness. Please report held-out RMSE and R^2 for every network used in Tables 1-2 and Fig. 7, and either re-run the verification with regression-matched networks or explicitly restrict the claim to 'the tested networks were verified at least as well under the chosen properties.'
  2. [Sect. 7.2, Eq. (25), Table 2] Property 5 is evaluated only with respect to the training dataset, which is the same data used to train both networks. Robustness measured on training points can reflect memorization rather than generalizable robustness, so the statement in Section 7.3 that 'Table 2 shows a marginal improvement in robustness performance' is not supported for unseen states. In addition, the naive network timed out for the epsilon=0.01 cells, so the adversarial network's 0% and 13.6% success rates in those cells have no naive baseline. Please re-evaluate Property 5 on a held-out test set, or at a minimum report the timeouts symmetrically and avoid interpreting cells that have no baseline as evidence of improvement or regression.
  3. [Sect. 3.2, Eq. (1), Table 3 (Appendix)] The dynamics used throughout are a simplification of the falling-plate model: Eq. (1) replaces tan alpha by x2/x1, and Section 3.2 constrains the angle of attack to [-pi/2,0]. The paper gives no quantitative validation that this simplified plant preserves the trajectories of the original model [24] or of real Alsomitra seeds. Since every verified property and reachable set in Sects. 7-8 concerns this simplified plant, the verification results are about a simulation model, not the physical drone; the title, abstract, and contributions should be adjusted accordingly. A concrete fix is to bound the error |tan alpha - x2/x1| over the reachable state space and to state explicitly that the case study certifies the simplified model, with the fidelity of that model listed as an assumption rather than an established fact.
  4. [Sect. 7.1, Property 4, Table 1] Property 4 is reported as y*=0 for every network. With the premise -x5 <= x6 <= -x5 + y*, setting y*=0 restricts the antecedent to a single line x6=-x5, which may be an empty or measure-zero subset of the valid input space, making the property vacuously true or trivially easy. The text says Property 4 'succeeded for all y* values' but does not discuss satisfiability of the antecedent. Please report whether the premise is satisfiable for each y*, and if the success is vacuous, remove or reframe the property so that Table 1 is not read as evidence of good behaviour.
minor comments (6)
  1. [Eq. (10)] The displayed formula contains (2y1+1)^4 ± (2y1+1)^4, which would make the two terms identical; the appendix version uses (2ℓCM/ℓ+1)^4 ± (2ℓCM/ℓ−1)^4, so the main-text equation is missing the sign change in the second factor. Please correct.
  2. [Table 2] The roles of epsilon rows and L* columns are not explicitly labeled in the table body; add a header such as 'epsilon \ L*' so that the orientation is unambiguous.
  3. [Fig. 7] Report quantitative bounds of the reachable sets (for example, the maximal |x6+x5| over the final reachable set) rather than only the plot, so the reader can assess how close the adversarial controller comes to the target trajectory.
  4. [Sect. 6 and Sect. 9.1] The DL2 and Gödel Logic PDT networks are not described in this paper and Section 9.1 notes differences in network structure; state their training hyperparameters and architecture or omit them from Tables 1 if they are not directly comparable.
  5. [Sect. 1.1] The text says 'All relevant files are publicly available here' but no URL appears in the manuscript; add the repository link for reproducibility.
  6. [Listing 3] The expression 'x ! i - x ! i + 6' is confusing; clarify that the network is doubled in onnx format and that indices 0-5 and 6-11 correspond to the same six states, so that the perturbation bound is expressed in the doubled-index representation.

Circularity Check

1 steps flagged · score 4.0 of 10

Partial circularity in the training-set robustness evaluation; core case-study and tool-comparison results are independent.

  1. fitted input called prediction [Section 7.2 (Property 5, Eq. 25, Listing 3), Section 7.3 (Table 2), Section 9.1 (limitation)]
    "due to Marabou limitations, this was evaluated with respect to the training dataset, where for each network Property 5 was evaluated for each training point, given fixed L∗ and ϵ values."

    Section 5 trains the adversarial network by PGD 'in an ϵ-ball around each training point (x, f(x))', and Property 5 then re-verifies the same ϵ-ball condition around the same training points. The perturbation set and the data used for the robustness evaluation are exactly the training objective's own input set, so Table 2 measures how well the training loss was optimised, not an independent generalisation guarantee. The paper's own limitation in Section 9.1, 'A better comparison could be made using NNs with equivalent regression performance on a test set of data, using a coefficient such as R2', confirms that the robustness comparison was not independent.

full rationale

The core case study is not circular: the dynamics are taken from an external falling-plate model [24], the PID training data and target trajectory x6 = -x5 are defined independently of the verification properties, and Properties 1-4 plus the CORA reachability task are universal statements over input boxes or initial sets, not fitted parameters. The comparison of verification tools (Marabou/Vehicle vs CORA) is externally grounded. The main circularity concern is localised to Property 5: robustness is evaluated on the same training dataset used to train the adversarial network, so Table 2 partly measures training fit. The paper candidly flags this and also notes that the naive-vs-adversarial reachability comparison could be confounded by differences in regression performance. There is also a minor self-citation in Section 5 ('Since the latter has been proven to be strictly stronger than the former in [6]') where the Lipschitz-robustness choice is justified by the authors' prior CAV paper, but that theorem is a simple implication and is not the paper's target result, so it does not materially raise the score. Overall the central in-principle feasibility claim retains independent content; the partial circularity is confined to the robustness-training evidence.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The verification claims rest on an externally sourced aerodynamic model, several simplifications made for tool tractability, and a behaviour-cloning dataset from a manually tuned PID controller. No new physical entities are introduced. The listed free parameters (PID gains, PGD epsilon, Lipschitz penalty weight, y* training threshold) are not reported with values, which limits reproduction.

free parameters (4)
  • PID gains for generating training data = manually tuned, not reported
    Section 4: the PID controller actuates y1 based on error in x6, and 'the gains are tuned manually until the control system performs well for a range of starting x6 positions.' These gains determine the behaviour-cloning dataset, so every learned controller and verification result inherits them.
  • PGD epsilon for adversarial training = not reported
    Section 5: adversarial training searches for worst-case examples in an epsilon-ball around each training point. The training epsilon is not listed; only verification epsilon values appear in Table 2.
  • Lipschitz penalty weight / dynamic L in loss = not reported
    Section 5: the highest L from training and adversarial points is 'summed to the training RMSE loss'. The relative weight of the Lipschitz penalty versus the RMSE term is unspecified.
  • y* threshold for PDT model training = 2
    Section 6: 'A value of y* = 2 was chosen for properties 1, 2, and 4 in training, in order to keep the properties relatively strict.' This hand-picked threshold shapes the DL2 and Gödel Logic models.
assumptions (5)
  • domain assumption Quasi-steady falling-plate aerodynamics accurately models Alsomitra gliding flight
    Section 3.1: 'Based on experimental measurements, our model accurately describes the falling trajectories of Alsomitra seeds by inferring aerodynamic forces from the angle of attack.' This is inherited from [24] and not revalidated in the paper.
  • domain assumption Infinitesimally thin plate and angle of attack in [-pi/2,0]
    Appendix Table 3: assumptions made for simplicity. They exclude thick-plate and post-stall regimes that real seeds may enter.
  • ad hoc to paper tan alpha approx x2/x1 (Eq 1) preserves flight behaviour
    Introduced to tame equation complexity. Section 1.1 states the CORA equations were simplified by constraining pitch and using an angle-of-attack definition; no comparison to the full model is given.
  • domain assumption Behaviour cloning from PID trajectories gives a representative input domain
    Section 4: training data come from 20 s PID simulations. Global properties are only quantified over inputs bounded by this training data (validInput), so states outside the PID envelope are unverified.
  • domain assumption Verification over the training-data-bounded input set implies safety for the ideal infinite-horizon property
    Section 4.1 reduces Eq (18) to finite-horizon and data-bounded tasks; no soundness argument connects the reduced properties back to the ideal one.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Neural Network Verification for Gliding Drone Control: A Case Study." pith.science (2026). https://pith.science/paper/ASSDIXYW

@misc{pith2026250500622,
  author       = {Pith},
  title        = {Pith review of: Neural Network Verification for Gliding Drone Control: A Case Study},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ASSDIXYW}},
  note         = {Machine review of arXiv:2505.00622}
}
read the original abstract

As machine learning is increasingly deployed in autonomous systems, verification of neural network controllers is becoming an active research domain. Existing tools and annual verification competitions suggest that soon this technology will become effective for real-world applications. Our application comes from the emerging field of microflyers that are passively transported by the wind, which may have various uses in weather or pollution monitoring. Specifically, we investigate centimetre-scale bio-inspired gliding drones that resemble Alsomitra macrocarpa diaspores. In this paper, we propose a new case study on verifying Alsomitra-inspired drones with neural network controllers, with the aim of adhering closely to a target trajectory. We show that our system differs substantially from existing VNN and ARCH competition benchmarks, and show that a combination of tools holds promise for verifying such systems in the future, if certain shortcomings can be overcome. We propose a novel method for robust training of regression networks, and investigate formalisations of this case study in Vehicle and CORA. Our verification results suggest that the investigated training methods do improve performance and robustness of neural network controllers in this application, but are limited in scope and usefulness. This is due to systematic limitations of both Vehicle and CORA, and the complexity of our system reducing the scale of reachability, which we investigate in detail. If these limitations can be overcome, it will enable engineers to develop safe and robust technologies that improve people's lives and reduce our impact on the environment.

Figures

Figures reproduced from arXiv: 2505.00622 by the authors.

Figure 1
Figure 1. An artist’s impression of a swarm of gliding drones inspired by Alsomitra seeds [7]. majority of ARCH-COMP cases, this problem does not have as natural a notion of the start, goal, safe, and unsafe states; and thus requires an out-of-the-box approach to property specification. We propose our ideal formalisation of the problem in Sect. 4.1, and distil the formalisation down to properties that can be handled with avai… view at source ↗
Figure 2
Figure 2. Overview of a negative feedback control system. For each control iteration, an error signal is calculated by subtracting the current system state (feedback) from the desired system state (input). A controller computes an actuation based on this error, which is applied to a simulated or real system (plant), resulting in some new output state. 2.2 Verification Tools The case study will rely on the following three grou… view at source ↗
Figure 3
Figure 3. General form of reachability specifications - dots represent the system at succes￾sive control time steps, and arrows represent the continuous trajectory of the system. Any trajectory starting in the initial set should never intersect an unsafe set, and always finish in the goal set. and CORA [2], see [25] for an exhaustive overview of the mainstream tools in this category. Representative benchmarks include simple d… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: (a) An Alsomitra seed [7]. (b) A two-dimensional approximation of an Alsomitra seed, with centre of mass (CoM) displaced by ℓCM (nondimensional form ex = ℓCM/ℓ). (c) Effect of various ex on gliding trajectories; according to a quasi-steady aerodynamic model ( [24], Sec…
Figure 5
Figure 5. Figure 5: As a control problem, we consider an Alsomitra-inspired microdrone and at￾tempt to follow a linear trajectory in two dimensions. As per the ARCH-COMP airplane and pendulum benchmarks [15], the neural network controller is trained using behaviour cloning. All simulation…
Figure 6
Figure 6. Figure 6: PID and basic NN controller performance on an Alsomitra-inspired drone. The naive network is trained on regression data obtained from simulations with the PID controller, and the resulting performance is similar but not perfect. ∀t ≥ t ∗ , ∀x1, ..., x6(0) ∈ R : |x6(t) …
Figure 7
Figure 7. Figure 7: Reachable regions in x5 and x6 for naive and adversarial NNs implemented as controllers, from the initial set defined in Eq. 26. The naive NN fails to reach a region bounded by y ∗ = 2 after 20 s, and the adversarial NN succeeds. This result shows significant improveme…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A General Framework for Property-Driven Machine Learning

    cs.LG 2025-05 conditional novelty 5.0 of 10

    A unified training objective generalizing adversarial training and differentiable-logic constraints, demonstrated on image classification and a drone controller.

Reference graph

Works this paper leans on

37 extracted references · 25 canonical work pages · cited by 1 Pith paper

  1. [24]

    Journal of Fluid Mechanics937, A6 (2022)

    Li, H., Goodwill, T., Jane Wang, Z., Ristroph, L.: Centre of mass location, flight modes, stability and dynamic modelling of gliders. Journal of Fluid Mechanics937, A6 (2022). https://doi.org/10.1017/jfm.2022.89

    doi:10.1017/jfm.2022.89 2022

  2. [1]

    In: 2019 IEEE International Sym- posium on Robotic and Sensors Environments (ROSE)

    Abouheaf, M., Mailhot, N., Gueaieb, W.: An online reinforcement learning wing- tracking mechanism for flexible wing aircraft. In: 2019 IEEE International Sym- posium on Robotic and Sensors Environments (ROSE). pp. 1–7 (2019).https: //doi.org/10.1109/ROSE.2019.8790425

    work page arXiv 2019

  3. [2]

    Althoff, M., Kochdumper, N., Ladner, T., Wetzlinger, M.: Manual v2025 (2024), https://tumcps.github.io/CORA/data/archive/manual/Cora2025Manual.pdf Neural Network Verification for Gliding Drone Control: A Case Study 19

    work page 2024

  4. [3]

    In: Proceedings of the Thirteenth In- ternational Conference on Machine Vision

    Amer, K., Samy, M., Shaker, M., ElHelw, M.: Deep convolutional neural net- work based autonomous drone navigation. In: Proceedings of the Thirteenth In- ternational Conference on Machine Vision. vol. 11605, p. 1160503 (2021).https: //doi.org/10.1117/12.2587105

    work page doi:10.1117/12.2587105 2021

  5. [4]

    Journal of The- oretical Biology129(3), 263–274 (1987).https://doi.org/https://doi.org/10

    Azuma, A., Okuno, Y.: Flight of a samara, alsomitra macrocarpa. Journal of The- oretical Biology129(3), 263–274 (1987).https://doi.org/https://doi.org/10. 1016/S0022-5193(87)80001-2

    work page 1987

  6. [5]

    Brix, C., Bak, S., Johnson, T.T., Wu, H.: The 5th international verification of neural networks competition (vnn-comp 2024): Summary and results (2024), https://www.arxiv.org/pdf/2412.19985

    arXiv 2024

  7. [6]

    Computer Aided Verification pp

    Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural network robustness as a verification property: A principled case study. Computer Aided Verification pp. 219–231 (2022)

    work page 2022

  8. [7]

    Phd thesis, University of Edin- burgh (February 2023)

    Certini, D.: The flight of Alsomitra macrocarpa. Phd thesis, University of Edin- burgh (February 2023)

    work page 2023

Show all 37 references
  1. [8]

    org/abs/2501.05867

    Cordeiro, L.C., Daggitt, M.L., Girard-Satabin, J., Isac, O., Johnson, T.T., Katz, G., Komendantskaya, E., Lemesle, A., Manino, E., Šinkarovs, A., Wu, H.: Neural network verification is a programming language challenge (2025),https://arxiv. org/abs/2501.05867

    2025 arXiv

  2. [9]

    Nature 562, 414–418 (2018),https://doi.org/10.1038/s41586-018-0604-2

    Cummins, C., Seale, M., Macente, A., Certini, D., Mastropaolo, E., Viola, I.M., Nakayama, N.: A separated vortex ring underlies the flight of the dandelion. Nature 562, 414–418 (2018),https://doi.org/10.1038/s41586-018-0604-2

    2018 doi

  3. [10]

    github.io/tutorial/

    Daggitt,M.,Kokke,W.,Komendantskaya,E.,Atkey,B.,Arnaboldi,L.,Slusarz,N., Casadio, M., Coke, B., Lee, J.: A vehicle tutorial (2024),https://vehicle-lang. github.io/tutorial/

    2024

  4. [11]

    ERC: A dandelion-inspired drone for swarm sensing.https://cordis.europa.eu/ project/id/101001499

  5. [12]

    Fischer, M., Balunović, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., Vechev, M.: Dl2:Trainingandqueryingneuralnetworkswithlogic.In:InternationalConference on Machine Learning (2019)

    2019

  6. [13]

    Flinkow, T., Casadio, M., Kessler, C., Monahan, R., Komendantskaya, E.: A Gen- eralised Framework for Property-Driven Machine Learning (2025), submitted to AI Verification

    2025

  7. [14]

    Science of Computer Programming244, 103280 (Sep 2025)

    Flinkow, T., Pearlmutter, B.A., Monahan, R.: Comparing differentiable logics for learning with logical constraints. Science of Computer Programming244, 103280 (Sep 2025). https://doi.org/10.1016/j.scico.2025.103280

    2025

  8. [15]

    workshop on applied verification for continuous and hybrid systems

    Frehse, G., Althoff, M.: Arch-comp24: Volume information proceedings of the 11th int. workshop on applied verification for continuous and hybrid systems. EPiC Series in Computing103(2024), https://easychair.org/publications/volume/ ARCH-COMP24

    2024

  9. [16]

    Nature603, 427–433 (2022)

    Iyer, V., Gaensbauer, H., Daniel, T.L., Gollakota, S.: Wind dispersal of battery-free wireless devices. Nature603, 427–433 (2022)

    2022

  10. [17]

    J. Li, Q. Yang, B.F.Y.S.: Robust state/output-feedback control of coaxial-rotor mavs based on adaptive nn approach (2019), https://ieeexplore.ieee.org/ document/8715436

    2019

  11. [18]

    Science Robotics8(82) (2023), https://www.science.org/doi/abs/10

    Johnson, K., Arroyos, V., Ferran, A., Villanueva, R., Yin, D., Elberier, T., Aliseda, A., Fuller, S., Iyer, V., Gollakota, S.: Solar-powered shape-changing origami mi- crofliers. Science Robotics8(82) (2023), https://www.science.org/doi/abs/10. 1126/scirobotics.adg4276 20 C. K...

    2023

  12. [19]

    Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: An efficient smt solver for verifying deep neural networks (2017), https://arxiv.org/abs/ 1702.01135

    2017 arXiv

  13. [20]

    443– 452 (2019)

    Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.: The marabou framework for verification and analysis of deep neural networks pp. 443– 452 (2019)

    2019

  14. [21]

    Nature (2021), https://doi.org/10.1038/s41586-021-03847-y

    Kim, B.H., Li, K., Kim, J.T., Park, Y., Jang, H., Wang, X., Xie, Z., Won, S.M., Yoon, H.J., Lee, G., Jang, W.J., Lee, K.H., Chung, T.S., Jung, Y.H., Heo, S.Y., Lee, Y., Kim, J., Cai, T., Kim, Y., Prasopsukh, P., Yu, Y., Yu, X., Avila, R., Luan, H., Song, H., Zhu, F., Zhao, Y.,...

    2021

  15. [22]

    NeurIPS 2018 tutorial (2018), available athttps://adversarial-ml-tutorial.org/

    Kolter, Z., Madry, A.: Adversarial robustness—theory and practice. NeurIPS 2018 tutorial (2018), available athttps://adversarial-ml-tutorial.org/

    2018

  16. [23]

    Lemesle, A., Lehmann, J., Le Gall, T.: Neural network verification with pyrat (2024), https://arxiv.org/abs/2410.23903

    2024 arXiv

  17. [25]

    EPiC Series in Computing103, 64–121 (2024),https://easychair.org/ publications/paper/WsgX

    Lopez, D.M., Althoff, M., Benet, L., Blab, C., Forets, M., Jia, Y., Johnson, T.T., Kranzl, M., Ladner, T., Linauer, L., Neubauer, P., Neubauer, S.A., Schilling, C., Zhang, H., Zhong, X.: Arch-comp24 category report: Artificial intelligence and neural network control systems (a...

    2024

  18. [26]

    Bionics and Sustainable Design (2022)

    Lumini, M.: Pherodrone1.0: An innovative inflatable uav’s concept, inspired by zanonia macrocarpa’s samara flying-wing and to insect’s sensillae, designed for the biological control of harmful insects in pa (precision agriculture). Bionics and Sustainable Design (2022)

    2022

  19. [27]

    com/eth-sri/eran

    Müller, M.N., Singh, G., Balunovic, M., Makarchuk, G., Ruoss, A., Serre, F., Baader, M., D Cohen, D., Gehr, T., Hoffmann, A., Maurer, J., Mirman, M., Müller, C., Püschel, M., Tsankov, P., Vechev, M.: Eran (2025),https://github. com/eth-sri/eran

    2025

  20. [28]

    IEEE Sensors Letters7(5), 1–4 (2023)

    Oshima, K., Kuribara, K., Sato, T.: Flex-snn: Spiking neural network on flexible substrate. IEEE Sensors Letters7(5), 1–4 (2023)

    2023

  21. [29]

    Springer, Cham (2018)

    Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63588-0

    2018 doi

  22. [30]

    IEEE Access 10, 91073–91091 (2022)

    Qamar, S., Khan, S.H., Arshad, M.A., Qamar, M., Gwak, J., Khan, A.: Au- tonomous drone swarm navigation and multitarget tracking with island policy- based optimization framework. IEEE Access 10, 91073–91091 (2022). https: //doi.org/10.1109/ACCESS.2022.3202208

    2022

  23. [31]

    IEEE Access12, 103026–103048 (2024).https://doi

    Richter, D.J., Calix, R.A., Kim, K.: A review of reinforcement learning for fixed- wing aircraft control tasks. IEEE Access12, 103026–103048 (2024).https://doi. org/10.1109/ACCESS.2024.3433540

    2024

  24. [32]

    Sensors22 (2022) Neural Network Verification for Gliding Drone Control: A Case Study 21

    Singaraju, S.A., Weller, D.D., Gspann, T.S., Aghassi-Hagmann, J., Tahoori, M.B.: Artificial neurons on flexible substrates: A fully printed approach for neuromorphic sensing. Sensors22 (2022) Neural Network Verification for Gliding Drone Control: A Case Study 21

    2022

  25. [33]

    Aerospace 8, 18 (2021)

    Wada, D., Araujo-Estrada, S.A., Windsor, S.: Unmanned aerial vehicle pitch con- trol using deep reinforcement learning with discrete actions in wind tunnel test. Aerospace 8, 18 (2021). https://doi.org/10.3390/aerospace8010018

    2021 doi

  26. [34]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems43(3), 994–1007 (2024)

    Wang, Y., Zhou, W., Fan, J., Wang, Z., Li, J., Chen, X., Huang, C., Li, W., Zhu, Q.: Polar-express: Efficient and precise formal reachability analysis of neural-network controlled systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems43(3), 994–...

    2024

  27. [35]

    Frontiers in Robotics and AI (2023)

    Wiesemüller, F., Meng, Z., Hu, Y., Farinha, A., Govdeli, Y., Nguyen, P.H., Nys- tröm, G., Kovač, M.: Transient bio-inspired gliders with embodied humidity re- sponsive actuators for environmental sensing. Frontiers in Robotics and AI (2023)

    2023

  28. [36]

    WMO: Global Demonstration Campaign for Evaluating the Use of Uncrewed Air- craft Systems in Operational Meteorology: White Paper. Tech. rep. (2023)

    2023

  29. [37]

    Advances in Neural Information Processing Systems31, 4939–4948 (2018), https://arxiv.org/pdf/ 1811.00866.pdf 10 Appendix 10.1 Equations 22 C

    Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural net- work robustness certification with general activation functions. Advances in Neural Information Processing Systems31, 4939–4948 (2018), https://arxiv.org/pdf/ 1811.00866.pdf 10 Appendix 10.1 Equa...

    2018 arXiv

Pith tools

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