Pith. sign in

REVIEW 3 major objections 3 minor 101 references

Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy

T0 review · 3 major / 3 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read This paper argues that verification and validation of vision-based autonomy can be unified: an interval-MDP abstraction is model-checked for safety and then validated on a new environment with Bayesian conformance, yielding an end-to-end PA

desk verdict The pipeline is real and runnable, but Theorem 2's OOD guarantee collapses a posterior probability into a frequentist confidence over datasets, so the headline claim is not established as written. read the letter →

arxiv 2508.14181 v1 pith:K3BVKNWS submitted 2025-08-19 eess.SY cs.ROcs.SY

Jordan Peper , Yan Miao , Sayan Mitra , Ivan Ruchkin This is my paper · ORCID
classification eess.SYcs.ROcs.SY
keywords neuralperceptionsafetyverificationprobabilisticvalidationintervalMarkovdecisionprocessvision-basedautonomydistributionshiftPACguaranteesBayesianmodelchecking
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 verification and validation of vision-based autonomy should be one process, not two. It builds an interval Markov decision process (IMDP) abstraction from training trajectories, model-checks a safety property on the abstraction to get a lower bound 1−β, and then uses Bayesian conformance on a validation dataset to measure whether the same abstraction still describes a new deployment environment. The central claim is Theorem 2: if the abstraction is statistically valid for the new environment with confidence at least 1−γ, then the new-environment system also satisfies the safety property with probability at least 1−β, with overall confidence at least 1−γ. If correct, this means safety guarantees degrade flexibly under distribution shift, and validation scores become quantitative safety evidence rather than qualitative alerts.

What carries the argument

The central object is the interval Markov decision process (IMDP) built by the paper's construction algorithms: transition probabilities are replaced by confidence intervals over abstract state tiles, so the model is a set of Markov chains rather than a single chain. This set is what makes the nested guarantee possible: verification computes the minimum safety probability over all distributions in the set, and validation measures how much posterior probability mass of the new environment's Dirichlet belief falls inside those same intervals. The bridge is the implication A ⇒ (B ⇒ C): if the new environment's true distribution lies in the abstraction's set, then any safety property verified on

What would settle it

Take a fixed IMDP and a fixed shifted environment, draw many independent validation datasets, and for each compute 1−γ with the paper's Algorithm 3; then measure the empirical frequency across those datasets with which the true system's safety probability is at least 1−β. If that frequency is far below the average value of 1−γ, Theorem 2's outer-probability reading is refuted.

Watch

Extended reading notes

Core claim

Put in the author's own terms: for a closed-loop system whose perception is a black-box neural estimator, one can (1) discretize state and estimation spaces, estimate transition probabilities from i.i.d. trajectories using exact binomial confidence intervals, and package them as an interval Markov decision process (IMDP) that over-approximates the ground-truth system with confidence 1−α; (2) run a probabilistic model checker on the IMDP to obtain a lower bound 1−β on the probability of satisfying a co-safe LTL property; and (3) on a validation dataset from a deployment environment, update a Dirichlet prior over the new environment's transition parameters and measure the posterior mass that f

Load-bearing premise

The load-bearing premise is that the Bayesian conformance confidence 1−γ, computed from one validation dataset, can be interpreted as a probability over random validation datasets; if it is only a subjective posterior belief, the law-of-total-probability step in Theorem 2 does not yield a frequentist guarantee.

Editorial extensions

If this is right

  • A safety lower bound verified on a training-environment abstraction can be exported to a deployment environment with a numerical confidence 1−γ, instead of requiring the deployment distribution to be known or bounded.
  • The median posterior conformance score can serve as a classifier: in the experiments, a threshold around 0.5 separated all tested in-distribution from out-of-distribution environments.
  • The method yields a tunable tradeoff: smaller α gives wider IMDP intervals, raising abstraction confidence and conformance but lowering the verified safety chance, so the user can select an operating point.
  • Because the IMDP over-approximates with 100% trajectory coverage in both case studies, the verified bounds are conservative; finer discretization improved safety chances but reduced conformance, revealing a resolution tradeoff.

Reading between the lines

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

  • The out-of-distribution guarantee would be stronger if the posterior conformance score were replaced or supplemented by a finite-sample concentration bound, so that 1−γ is a frequentist coverage guarantee over validation datasets rather than a posterior degree of belief.
  • The per-state Dirichlet integration is Monte Carlo; a distribution-free alternative, such as conformal containment of the true transition vector in the interval set, could yield coverage guarantees that hold for every dataset rather than on average.
  • The median aggregation sacrifices worst-case safety for robustness; an adversary could place a dangerous state with low conformance below the median. A verification-weighted aggregation over states that dominate the safety probability would make the system-level γ reflect the states that matter.
  • The roughly 0.2 Jaccard similarity between real and abstract transitions suggests the abstraction is loose; adaptive tiling or state-dependent granularity could tighten verification without losing validation discrimination.
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

3 major / 3 minor

Summary. The paper proposes a three-stage framework for vision-based autonomous systems. Stage 1 (Sec. 4.1) collects trajectories from a training environment, discretizes the state/estimate space, computes Clopper-Pearson confidence intervals for transition probabilities, and builds an IMDP abstraction. Stage 2 (Sec. 4.2) model-checks a co-safe LTL property on the IMDP with PRISM/Storm to obtain a lower bound 1−β on the safety probability. Stage 3 (Sec. 4.3) takes a validation dataset from a possibly different environment, updates a Dirichlet prior over transition parameters, computes a per-state posterior conformance probability that the parameters fall inside the training intervals, and aggregates these by the median. The formal results are Theorem 1 (in-distribution: with confidence 1−α over training data, the concrete system is safe with probability ≥1−β) and Theorem 2 (out-of-distribution: with confidence 1−γ over validation data, the new system is safe with probability ≥1−β). Experiments on a synthetic goal-reaching system and a vision-based mountain car demonstrate that the conformance metric separates in-distribution from out-of-distribution environments and illustrate tradeoffs between safety chance and validation confidence.

Significance. If Theorem 2 were valid, this would be a notable contribution: a data-driven IMDP abstraction with a PAC-style safety certificate that degrades gracefully under distribution shift, together with an offline validation procedure. The paper is clearly written, releases code, and includes two case studies with concrete model-checking results. However, the central OOD guarantee is not established as stated, and the validation procedure is not shown to instantiate the theorem's main assumption. As it stands, the paper provides a useful heuristic for OOD conformance monitoring and a conditional in-distribution result, but not the advertised end-to-end probabilistic guarantee.

major comments (3)
  1. [Sec. 4.3, Def. 7, Eq. (4), Thm. 2, App. A.2] The OOD theorem is not established. Definition 7 defines γ through the posterior M_po, which is computed from the observed D_val; the conclusion of Theorem 2, however, is a probability over D_val. In the proof, event A is assigned probability ≥1−γ by Definition 7 and then used in the law of total probability as if it were a frequency over validation datasets. Since 1−γ is a posterior belief conditional on a fixed D_val (hence a random variable when D_val is random), the inequality Pr_{D_val}[...]≥1−γ does not follow without a calibration result linking posterior coverage to frequentist coverage. No such result or simulation-based coverage check is provided. A purely conditional statement ('with posterior probability ≥1−γ after seeing D_val, ...') would be valid, but it is not the PAC-style guarantee claimed.
  2. [Sec. 4.3, Algorithm 3, Def. 7] The γ in Definition 7 is a system-level posterior conformance probability, but Algorithm 3 computes per-state confidences and aggregates them by the median, with no argument that median(Γ) equals or lower-bounds the probability of the joint event that the new model's full transition structure lies in the IMDP. The worst-case min confidence is mentioned but rejected. Thus the 1−γ values reported in Table 2 and Figures 2/4 are not shown to instantiate the premise of Theorem 2.
  3. [Sec. 4.1, Algorithm 1, Def. 2, Thm. 1] Algorithm 1 places a Bonferroni correction α/(2N) over the N estimate bins of each state, which gives per-state joint coverage at level 1−α if a union bound is applied over those N intervals. But Definition 2 requires the global event that the trajectory distribution is contained in the IMDP, i.e., simultaneous coverage over all states (and all transitions used along trajectories). No union bound over the number of states is applied, so the construction does not, as stated, yield the statistically sound abstraction required by Theorem 1.
minor comments (3)
  1. [Thm. 1 and Thm. 2 statements] The inner probability in both theorems is written Pr_{τ∼JMEK}(τ⊨φ), i.e., over the IMDP semantics. If taken literally, the conclusions are trivial given the second premises. The proofs in Appendices A.1 and A.2 use event C for the concrete system ME (resp. ME′). Please correct the notation to distinguish the abstract semantics from the concrete trajectory semantics.
  2. [Sec. 4.3, Eqs. (7)-(8)] The Monte Carlo approximation in Eq. (8) introduces sampling error that is not reflected in γ. The theorem treats γ as exact; to support the formal claim, the number of samples N should be accompanied by a finite-sample concentration bound or the approximation error should be absorbed conservatively into γ.
  3. [Sec. 4.3, Alg. 3, Table 2] The sign convention for γ is inconsistent: Definition 7 uses 1−γ as the posterior probability (with γ as the error), while the text says 'γ=median(Γ)' with Γ containing 1−γ_s. The reported '1−γ' column in Table 2 appears to be a conformance probability, not an error probability. Please harmonize the notation.

Circularity Check

1 steps flagged · score 6.0 of 10

Theorem 2's OOD guarantee uses the data-fitted posterior conformance γ as its confidence level; the proof conflates posterior probability with dataset frequency.

  1. fitted input called prediction [Definition 7, Eq. (4); Section 4.3, Theorem 2; Appendix A.2]
    "Definition 7: PrMpo (JMK∈JM EK|M∼M po)≥1−γ ... Theorem 2: PrDval [ Prτ∼JM E K (τ⊨φ)≥1−β ]≥1−γ ... Proof: A≜JMK∈JM EK|M∼M po is the event that a model in our posterior distribution over models exists within the IMDP (statistical validity Def. 7)."

    Definition 7 defines γ as the posterior probability, after seeing the validation dataset D_val, that the new system's model lies in the IMDP. Theorem 2 then concludes a probability over the random variable D_val with confidence 1−γ. The proof applies the law of total probability to Pr(A)≥1−γ, treating the posterior probability (conditional on the observed data) as if it were a marginal frequency over D_val. Thus the confidence level 1−γ in the conclusion is exactly the quantity fitted/computed from D_val in Eqs. (4)–(8); the 'prediction' of OOD safety is wrapped in the same data-dependent γ. No calibration argument connects the posterior coverage to frequentist coverage over D_val, so the guarantee is a restatement of the posterior conformance score rather than an independent PAC bound.

full rationale

The paper's Theorem 1 is a genuine conditional/total-probability argument: the α-soundness event from Definition 2 is a frequentist statement over D_train, the safety bound 1−β is independently model-checked, and the conclusion follows by law of total probability. That part is not circular. The central OOD claim, Theorem 2, is different: its premise 'statistically γ-valid abstraction' is defined in Definition 7 as a posterior probability over models given the fixed dataset D_val, yet its conclusion is a probability over the random dataset D_val with confidence 1−γ. The proof implicitly replaces the posterior probability with a marginal probability over D_val, making the data-fitted γ serve both as input and as output confidence. This is a fitted-input-called-prediction pattern: the conformance score computed from D_val is renamed as the confidence of an end-to-end safety guarantee over D_val. The safety probability 1−β is independently obtained from model checking, so the circularity is partial rather than total, but the paper's advertised flexible OOD guarantee reduces to the posterior conformance score without an independent probabilistic justification.

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

The central claims rest on several weakly justified premises. The most fragile is treating the Bayesian posterior conformance as a frequentist confidence over validation datasets, which is exactly the step that makes Theorem 2 an end-to-end guarantee. Property preservation under abstraction, i.i.d. trajectory sampling, and median aggregation are also assumed rather than proved.

free parameters (5)
  • Binomial confidence level alpha = 0.05 in main results; varied 0.001 to 0.3 in tradeoff experiments
    Chosen by the user; controls the width of the Clopper-Pearson intervals and directly drives the reported safety chance and conformance confidence.
  • Discretization tile sizes = 0.5 units for the synthetic system; x:0.05, v:0.005, estimation error:0.1 for mountain car
    Hand-chosen modeling parameters; the paper's own ablation shows the safety chance varies from 0.036 to 0.9998 with tile size, so results are strongly dependent on this choice.
  • Dirichlet prior concentration alpha_0 = 1 (uniform) for all states
    Chosen by hand; initializes the posterior used to compute the conformance confidence gamma.
  • Monte Carlo sample count N = not specified
    Number of Dirichlet samples used in Eq. 8 and Algorithm 3 is never reported, so the precision of the conformance confidence is not reproducible.
  • Validation environment noise bounds = Training uses sigma-squared = 0.5; ID validation is described with sigma-squared in [0.5, 4.0]
    Environment parameters chosen for the experiments; describing the validation environment as in-distribution despite a different noise range is inconsistent and affects the ID/OOD labeling.
assumptions (6)
  • domain assumption Abstraction is property-preserving: if psi(tau) satisfies phi then tau satisfies phi
    Used in the proofs of Theorems 1 and 2 (Appendix A.1 and A.2). Algorithm 2 over-approximates reachable cells, but the paper does not prove this monotonicity for arbitrary LTL/PCTL properties or non-monotone dynamics.
  • domain assumption Training data D_train consists of i.i.d. trajectories from the closed-loop system distribution
    Definition 2 requires this. Sections 5.1 and 5.2 instead place the agent at each state tile and collect per-tile estimates, which is not i.i.d. trajectory sampling from the closed-loop distribution.
  • ad hoc to paper Posterior conformance probability can be used as a frequentist confidence over validation data
    Theorem 2 and its proof treat gamma from Definition 7 and Eq. 4 as an outer probability over D_val, conflating Bayesian belief with sampling probability. No calibration argument is provided.
  • ad hoc to paper Median of per-state conformance confidences equals system-level validity confidence
    Section 4.3 selects the median without a theorem or calibration argument; the authors note the minimum is too conservative but do not justify the median as sound.
  • domain assumption Per-state transitions are stationary and independent given an abstract state
    Algorithm 1 counts estimate occurrences per abstract state and uses binomial/multinomial intervals, assuming independence across visits and no temporal dependence. This is not stated as an assumption.
  • standard math Bayes' theorem and the law of total probability
    Unproved background results invoked in Section 4.3 and in the Appendix proofs.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy." pith.science (2026). https://pith.science/paper/K3BVKNWS

@misc{pith2026250814181,
  author       = {Pith},
  title        = {Pith review of: Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/K3BVKNWS}},
  note         = {Machine review of arXiv:2508.14181}
}
read the original abstract

Precise and comprehensive situational awareness is a critical capability of modern autonomous systems. Deep neural networks that perceive task-critical details from rich sensory signals have become ubiquitous; however, their black-box behavior and sensitivity to environmental uncertainty and distribution shifts make them challenging to verify formally. Abstraction-based verification techniques for vision-based autonomy produce safety guarantees contingent on rigid assumptions, such as bounded errors or known unique distributions. Such overly restrictive and inflexible assumptions limit the validity of the guarantees, especially in diverse and uncertain test-time environments. We propose a methodology that unifies the verification models of perception with their offline validation. Our methodology leverages interval MDPs and provides a flexible end-to-end guarantee that adapts directly to the out-of-distribution test-time conditions. We evaluate our methodology on a synthetic perception Markov chain with well-defined state estimation distributions and a mountain car benchmark. Our findings reveal that we can guarantee tight yet rigorous bounds on overall system safety.

Figures

Figures reproduced from arXiv: 2508.14181 by the authors.

Figure 1
Figure 1. Our verification & validation methodology in three steps. Running example. We utilize the OpenAI Gym [12] MountainCar-v0 benchmark (a widely adopted testbed for reinforcement learning) as a running example to clarify the algorithms throughout this section. This environment models a two-dimensional control problem with state variables s = (x, v) ∈ [−1.2, 0.6] × [−0.07, 0.07], where x is the horizontal position of the… view at source ↗
Figure 2
Figure 2. Safety chance and conformance confidence are tradeoffs as functions of α for the goal-reaching system. A smaller α corresponds to higher binomial confidence, leading to looser IMDP intervals, thus providing the model checker with greater flexibility to select worst-case distributions, resulting in lower safety chances. Discriminating ID and OOD systems. To demonstrate the discriminative ability of our validation, we… view at source ↗
Figure 3
Figure 3. Examples of noisy visual inputs from the MountainCar environment. The true car position is fixed at −0.46. The position estimation errors are 0.01, 0.25, 0.46, and 0.58 from left to right. Abstraction. To construct an α-sound abstraction of the MountainCar, we de￾fine an abstraction function ψ using uniform discretization with bins of size [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Safety chance and conformance confidence are tradeoffs as functions of α for the mountain car, analogous to [PITH_FULL_IMAGE:figures/full_fig_p020_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

101 extracted references · 50 canonical work pages

  1. [1]

    Formal Methods in System Design54(3), 416–448 (Nov 2019).https://doi.org/10.1007/s10703-019-00333-0,https://doi.org/10

    Aichernig, B.K., Tappler, M.: Probabilistic black-box reachability checking (extended version). Formal Methods in System Design54(3), 416–448 (Nov 2019).https://doi.org/10.1007/s10703-019-00333-0,https://doi.org/10. 1007/s10703-019-00333-0

    doi:10.1007/s10703-019-00333-0 2019

  2. [2]

    Journal of Systems and Software 188, 111275 (Jun 2022).https://doi.org/10.1016/j.jss.2022.111275,https: //www.sciencedirect.com/science/article/pii/S016412122200036X

    Alasmari, N., Calinescu, R., Paterson, C., Mirandola, R.: Quantitative verifi- cation with adaptive uncertainty reduction. Journal of Systems and Software 188, 111275 (Jun 2022).https://doi.org/10.1016/j.jss.2022.111275,https: //www.sciencedirect.com/science/article/pii/S016412122200036X

    work page arXiv 2022

  3. [3]

    Proceedings of the ACM on Programming Lan- guages7(OOPSLA2), 2196–2223 (Oct 2023).https://doi.org/10.1145/3622875, https://dl.acm.org/doi/10.1145/3622875

    Astorga, A., Hsieh, C., Madhusudan, P., Mitra, S.: Perception Contracts for Safety of ML-Enabled Systems. Proceedings of the ACM on Programming Lan- guages7(OOPSLA2), 2196–2223 (Oct 2023).https://doi.org/10.1145/3622875, https://dl.acm.org/doi/10.1145/3622875

    doi:10.1145/3622875 2023

  4. [4]

    International Journal on Software Tools for Technology Transfer24(5), 803–819 (Oct 2022).https://doi.org/10.1007/s10009-022-00673-z,https://doi.org/10

    Badings, T., Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Scenario-based verification of uncertain parametric MDPs. International Journal on Software Tools for Technology Transfer24(5), 803–819 (Oct 2022).https://doi.org/10.1007/s10009-022-00673-z,https://doi.org/10. 1007/s10009-022-00673-z

    doi:10.1007/s10009-022-00673-z 2022

  5. [5]

    35th International Conference on Computer Aided Verification (Apr 2023)

    Badings, T., Junges, S., Marandi, A., Topcu, U., Jansen, N.: Efficient Sensitivity Analysis for Parametric Robust Markov Chains. 35th International Conference on Computer Aided Verification (Apr 2023)

    2023

  6. [6]

    Badithela, A., Wongpiromsarn, T., Murray, R.M.: Evaluation Metrics for Ob- ject Detection for Autonomous Systems (Oct 2022).https://doi.org/10.48550/ arXiv.2210.10298,http://arxiv.org/abs/2210.10298, arXiv:2210.10298 [cs, eess]

    work page Pith review arXiv doi:10.48550/arxiv.2210.10298 2022

  7. [7]

    Computer54(12), 50–59 (Dec 2021).https://doi.org/ 10.1109/MC.2021.3085532,https://ieeexplore.ieee.org/document/9622291/

    Bakirtzis,G.,Subrahmanian,E.,Fleming,C.H.:CompositionalThinkinginCyber- physical Systems Theory. Computer54(12), 50–59 (Dec 2021).https://doi.org/ 10.1109/MC.2021.3085532,https://ieeexplore.ieee.org/document/9622291/

    work page arXiv 2021

  8. [8]

    In: Steffen, B

    Bensalem, S., Cheng, C.H., Huang, W., Huang, X., Wu, C., Zhao, X.: What, In- deed, is an Achievable Provable Guarantee for Learning-Enabled Safety-Critical Systems. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality. pp. 55–76. Springer Nature Switzerland, Cham (2024).https://doi.org/10.1007/ 978-3-031-46002-9_4

    2024

Show all 101 references
  1. [9]

    4273–4279 (2017),https://www.ijcai.org/ proceedings/2017/597

    Bharadwaj, S., Roux, S.L., Perez, G., Topcu, U.: Reduction Techniques for Model Checking and Learning in MDPs pp. 4273–4279 (2017),https://www.ijcai.org/ proceedings/2017/597

    2017

  2. [10]

    SIGSOFT Softw

    Blundell, C., Giannakopoulou, D., Pˇ asˇ areanu, C.S.: Assume-guarantee testing. SIGSOFT Softw. Eng. Notes31(2), 1–es (Sep 2005).https://doi.org/10.1145/ 1118537.1123060,https://dl.acm.org/doi/10.1145/1118537.1123060

    2005

  3. [11]

    Bojarski, M., Del Testa, D., Dworakowski, D., Firner, B., Flepp, B., Goyal, P., Jackel,L.D.,Monfort,M.,Muller,U.,Zhang,J.,Zhang,X.,Zhao,J.,Zieba,K.:End to End Learning for Self-Driving Cars (Apr 2016).https://doi.org/10.48550/ arXiv.1604.07316,http://arxiv.org/abs/1604.07316, ...

    2016 doi arXiv

  4. [12]

    01540,http://arxiv.org/abs/1606.01540, arXiv:1606.01540 [cs]

    Brockman, G., Cheung, V., Pettersson, L., Schneider, J., Schulman, J., Tang, J., Zaremba,W.:OpenAIGym(Jun2016).https://doi.org/10.48550/arXiv.1606. 01540,http://arxiv.org/abs/1606.01540, arXiv:1606.01540 [cs]

    doi arXiv

  5. [13]

    IEEE Transactions on Software Engineer- ing (2024),https://www.computer.org/csdl/journal/ts/2024/06/10496502/ 1W28Vqz3hQc

    Calinescu, R., Imrie, C., Mangal, R., Rodrigues, G.N., Păsăreanu, C., San- tana, M.A., Vázquez, G.: Controller Synthesis for Autonomous Systems With 22 Jordan Peper, Yan Miao, Sayan Mitra, and Ivan Ruchkin Deep-Learning Perception Components. IEEE Transactions on Software Engi...

    2024

  6. [14]

    In: 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS’21) (2021), arXiv: 2104.15006

    Carpenter, T.J., Ivanov, R., Lee, I., Weimer, J.: ModelGuard: Runtime Validation of Lipschitz-continuous Models. In: 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS’21) (2021), arXiv: 2104.15006

    2021 arXiv

  7. [15]

    Cauchois, M., Gupta, S., Ali, A., Duchi, J.C.: Robust Validation: Confident Pre- dictions Even When Distributions Shift. Journal of the American Statistical As- sociation0(0), 1–66 (2024).https://doi.org/10.1080/01621459.2023.2298037, https://doi.org/10.1080/01621459.2023.2298...

    2024

  8. [16]

    Ph.D., University of California, Berkeley, United States – California (2020),https://www.proquest.com/docview/2460739262/abstract/ 18015E97A18F4C45PQ/1, iSBN: 9798678171221

    Chapman, M.P.: Risk-Sensitive Safety Analysis and Control for Trustwor- thy Autonomy. Ph.D., University of California, Berkeley, United States – California (2020),https://www.proquest.com/docview/2460739262/abstract/ 18015E97A18F4C45PQ/1, iSBN: 9798678171221

    2020

  9. [17]

    48550/arXiv.2503.18077,http://arxiv.org/abs/2503.18077, arXiv:2503.18077 [cs] version: 2

    Cleaveland, M., Lu, P., Sokolsky, O., Lee, I., Ruchkin, I.: Conservative Per- ception Models for Probabilistic Verification (Apr 2025).https://doi.org/10. 48550/arXiv.2503.18077,http://arxiv.org/abs/2503.18077, arXiv:2503.18077 [cs] version: 2

    2025 doi arXiv

  10. [19]

    In: Proc

    Cleaveland, M., Sokolsky, O., Lee, I., Ruchkin, I.: Conservative Safety Monitors of Stochastic Dynamical Systems. In: Proc. of the NASA Formal Methods Conference (May 2023)

    2023

  11. [20]

    Journal of Artificial Intelligence Research72, 377–428 (Jan 2022).https://doi.org/10.1613/jair

    Corso, A., Moss, R., Koren, M., Lee, R., Kochenderfer, M.: A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems. Journal of Artificial Intelligence Research72, 377–428 (Jan 2022).https://doi.org/10.1613/jair. 1.12716,https://dl.acm.org/doi/10.1613/j...

    2022 doi

  12. [21]

    In: Tools and Algorithms for the Construc- tion and Analysis of Systems

    Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Scenario-Based Verification of Uncertain MDPs. In: Tools and Algorithms for the Construc- tion and Analysis of Systems. pp. 287–305. Lecture Notes in Computer Sci- ence,SpringerInternationalPublishing,Cham(2020).h...

    2020

  13. [22]

    In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering

    Cámara, J.: HaiQ: Synthesis of Software Design Spaces with Structural and Proba- bilistic Guarantees. In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering. pp. 22–33. FormaliSE ’20, Association for Com- puting Machinery, New York, NY, U...

    2020

  14. [23]

    In: Pro- ceedings of the 15th ACM international conference on Hybrid Systems: Computa- tion and Control

    D’Innocenzo, A., Abate, A., Katoen, J.P.: Robust PCTL model checking. In: Pro- ceedings of the 15th ACM international conference on Hybrid Systems: Computa- tion and Control. pp. 275–286. HSCC ’12, Association for Computing Machinery, New York, NY, USA (Apr 2012).https://doi.o...

    2012

  15. [24]

    Dong, Y., Huang, W., Bharti, V., Cox, V., Banks, A., Wang, S., Zhao, X., Schewe, S., Huang, X.: Reliability Assessment and Safety Arguments for Machine Learn- ing Components in System Assurance. ACM Transactions on Embedded Comput- ing Systems22(3), 48:1–48:48 (Apr 2023).https...

    2023 doi

  16. [25]

    Dong, Y., Huang, J., Ai, J.: Visual Perception-Based Target Aircraft Move- ment Prediction for Autonomous Air Combat. Journal of Aircraft52(2), 538–552 (Mar 2015).https://doi.org/10.2514/1.C032764,https://arc.aiaa.org/doi/ 10.2514/1.C032764, publisher: American Institute of Ae...

    2015 doi

  17. [26]

    IEEE Transactions on Aerospace and Electronic Systems57(4), 2346–2368 (Aug 2021).https://doi.org/10

    Dong, Y., Tao, J., Zhang, Y., Lin, W., Ai, J.: Deep Learning in Aircraft Design, Dynamics, and Control: Review and Prospects. IEEE Transactions on Aerospace and Electronic Systems57(4), 2346–2368 (Aug 2021).https://doi.org/10. 1109/TAES.2021.3056086,https://ieeexplore.ieee.org...

    2021

  18. [27]

    Journal of Automated Reasoning 63(4), 1031–1053 (Dec 2019).https://doi.org/10.1007/s10817-018-09509-5, https://doi.org/10.1007/s10817-018-09509-5

    Dreossi, T., Donzé, A., Seshia, S.A.: Compositional Falsification of Cyber-Physical Systems with Machine Learning Components. Journal of Automated Reasoning 63(4), 1031–1053 (Dec 2019).https://doi.org/10.1007/s10817-018-09509-5, https://doi.org/10.1007/s10817-018-09509-5

    2019 doi

  19. [28]

    arXiv:1902.04245 [cs] (Feb 2019), http://arxiv.org/abs/1902.04245, arXiv: 1902.04245

    Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Ravanbakhsh, H., Vazquez- Chanlatte, M., Seshia, S.A.: VERIFAI: A Toolkit for the Design and Anal- ysis of Artificial Intelligence-Based Systems. arXiv:1902.04245 [cs] (Feb 2019), http://arxiv.org/abs/1902.04245, arXiv: 1902.04245

    1902 arXiv

  20. [29]

    In: Proc

    Dutta, S., Caprio, M., Lin, V., Cleaveland, M., Jang, K.J., Ruchkin, I., Sokolsky, O., Lee, I.: Distributionally Robust Statistical Verification with Imprecise Neural Networks. In: Proc. of HSCC 2025. Springer (2025).https://doi.org/10.48550/ arXiv.2308.14815

    2025 doi arXiv

  21. [30]

    International Journal on Soft- ware Tools for Technology Transfer17(4), 469–484 (2015)

    D’Argenio, P., Legay, A., Sedwards, S., Traonouez, L.M.: Smart sampling for lightweight verification of markov decision processes. International Journal on Soft- ware Tools for Technology Transfer17(4), 469–484 (2015)

    2015

  22. [31]

    Theoretical Computer Science410(42), 4262– 4291 (Sep 2009).https://doi.org/10.1016/j.tcs.2009.06.021,http://www

    Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science410(42), 4262– 4291 (Sep 2009).https://doi.org/10.1016/j.tcs.2009.06.021,http://www. sciencedirect.com/science/article/pii/S0304397509004149

    2009 doi

  23. [32]

    In: Proc

    Feng, L., Han, T., Kwiatkowska, M., Parker, D.: Learning-Based Compositional Verification for Synchronous Probabilistic Systems. In: Proc. of ATVA. pp. 511–

  24. [33]

    Filos, A., Tigkas, P., Mcallister, R., Rhinehart, N., Levine, S., Gal, Y.: Can Autonomous Vehicles Identify, Recover From, and Adapt to Distribution Shifts? In: Proceedings of the 37th International Conference on Machine Learn- ing. pp. 3145–3153. PMLR (Nov 2020),https://proce...

    2020

  25. [34]

    Wiley-Interscience, Hoboken, N.J, 3rd edn

    Fleiss, J.L., Levin, B., Paik, M.C.: Statistical Methods for Rates & Proportions. Wiley-Interscience, Hoboken, N.J, 3rd edn. (2003)

    2003

  26. [35]

    In: Proc

    Frehse, G., Han, Z., Krogh, B.: Assume-guarantee reasoning for hybrid I/O- automata by over-approximation of continuous interaction. In: Proc. of the 43rd IEEE Conference on Decision and Control (CDC) (IEEE Cat. No.04CH37601). vol. 1, pp. 479–484 Vol.1 (Dec 2004).https://doi.o...

    2004 doi

  27. [36]

    International Journal on Soft- ware Tools for Technology Transfer24(5), 667–689 (Oct 2022).https://doi.org/ 10.1007/s10009-022-00669-9,https://doi.org/10.1007/s10009-022-00669-9

    Frenkel,H.,Grumberg,O.,Păsăreanu,C.S.,Sheinvald,S.:Assume,guaranteeorre- pair: a regular framework for non regular properties. International Journal on Soft- ware Tools for Technology Transfer24(5), 667–689 (Oct 2022).https://doi.org/ 10.1007/s10009-022-00669-9,https://doi.org...

    2022 doi

  28. [37]

    Robotics: Science and Sys- tems X (Jul 2014).https://doi.org/10.15607/RSS.2014.X.039,http://www

    Fu, J., Topcu, U.: Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints. Robotics: Science and Sys- tems X (Jul 2014).https://doi.org/10.15607/RSS.2014.X.039,http://www. 24 Jordan Peper, Yan Miao, Sayan Mitra, and Ivan Ruchkin roboticsproceed...

    2014 doi

  29. [38]

    In: Embedded Systems Development, pp

    Graf, S., Passerone, R., Quinton, S.: Contract-Based Reasoning for Component Systems with Rich Interactions. In: Embedded Systems Development, pp. 139–

  30. [39]

    arXiv:2006.10564 [cs, math, stat] (Feb 2022),http://arxiv.org/abs/2006.10564, arXiv: 2006.10564

    Gupta, C., Podkopaev, A., Ramdas, A.: Distribution-free binary classification: pre- diction sets, confidence intervals and calibration. arXiv:2006.10564 [cs, math, stat] (Feb 2022),http://arxiv.org/abs/2006.10564, arXiv: 2006.10564

    2006 arXiv

  31. [40]

    07080,http://arxiv.org/abs/2002.07080, arXiv:2002.07080 [cs]

    Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The Probabilis- tic Model Checker Storm (Oct 2020).https://doi.org/10.48550/arXiv.2002. 07080,http://arxiv.org/abs/2002.07080, arXiv:2002.07080 [cs]

    2020 doi arXiv

  32. [41]

    In: Computer Aided Verification

    Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T., Seshia, S.A., Van den Broeck, G.: Model Checking Finite-Horizon Markov Chains with Probabilistic In- ference. In: Computer Aided Verification. pp. 577–601. Lecture Notes in Computer Science, Springer International ...

    2021

  33. [42]

    arXiv:1705.09970 [cs] (Jul 2017),http://arxiv.org/abs/1705.09970, arXiv: 1705.09970

    Holtzen, S., Millstein, T., Broeck, G.V.d.: Probabilistic Program Abstractions. arXiv:1705.09970 [cs] (Jul 2017),http://arxiv.org/abs/1705.09970, arXiv: 1705.09970

    2017 arXiv

  34. [43]

    Dover Publications, New York, 1 edn

    Howard, R.A.: Dynamic Probabilistic Systems, Volume II: Semi-Markov and De- cision Processes. Dover Publications, New York, 1 edn. (Jun 2007)

    2007

  35. [44]

    IEEE Trans

    Hsieh, C., Li, Y., Sun, D., Joshi, K., Misailovic, S., Mitra, S.: Verify- ing controllers with vision-based perception using safe approximate abstrac- tions. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.41(11), 4205– 4216 (2022).https://doi.org/10.1109/TCAD.2022.319750...

    2022

  36. [45]

    In: Computer Aided Verification

    Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety Verification of Deep Neural Networks. In: Computer Aided Verification. pp. 3–29. Lecture Notes in Computer Science, Springer International Publishing, Cham (2017).https://doi.org/10. 1007/978-3-319-63387-9_1

    2017

  37. [46]

    In: NASA Formal Methods: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings

    Incer, I., Benveniste, A., Sangiovanni-Vincentelli, A., Seshia, S.A.: Hypercontracts. In: NASA Formal Methods: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. pp. 674–692. Springer-Verlag, Berlin, Heidelberg (May 2022),https://doi.org/1...

    2022 doi

  38. [47]

    In: Proceedings of the 23rd International Conference on Hybrid Systems: Com- putation and Control

    Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Case study: verifying the safety of an autonomous racing car with a neural network controller. In: Proceedings of the 23rd International Conference on Hybrid Systems: Com- putation and Control. pp. 1–7. ...

    2020

  39. [48]

    Jackson, J., Laurenti, L., Frew, E., Lahijanian, M.: Formal Verifi- cation of Unknown Dynamical Systems via Gaussian Process Re- gression (Dec 2021),https://www.semanticscholar.org/paper/ Formal-Verification-of-Unknown-Dynamical-Systems-Jackson-Laurenti/ 8093250cc2b5876880717a...

    2021

  40. [49]

    In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

    Katoen, J.P.: The Probabilistic Model Checking Landscape. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 31–

  41. [50]

    ACM Transactions on Graphics42(4) (July 2023),https://repo-sam.inria.fr/fungraph/3d-gaussian-splatting/

    Kerbl, B., Kopanas, G., Leimkühler, T., Drettakis, G.: 3d gaussian splatting for real-time radiance field rendering. ACM Transactions on Graphics42(4) (July 2023),https://repo-sam.inria.fr/fungraph/3d-gaussian-splatting/

    2023

  42. [51]

    arXiv:1207.5086 [cs]7358, 310–326 (2012).https://doi.org/10.1007/978-3-642-31424-7_25,http://arxiv.org/ abs/1207.5086, arXiv: 1207.5086

    Komuravelli, A., Pasareanu, C.S., Clarke, E.M.: Assume-Guarantee Abstrac- tion Refinement for Probabilistic Systems. arXiv:1207.5086 [cs]7358, 310–326 (2012).https://doi.org/10.1007/978-3-642-31424-7_25,http://arxiv.org/ abs/1207.5086, arXiv: 1207.5086

    2012 arXiv

  43. [52]

    LICS ’16, Association for Computing Machinery, New York, NY, USA (Jul 2016).https://doi.org/10.1145/2933575.2934574,https://doi.org/10.1145/ 2933575.2934574 Towards Unified Probabilistic Verification and Validation 25

    2016

  44. [53]

    In: Bernardo, M., Hillston, J

    Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for Performance Eval- uation, pp. 220–270. No. 4486 in Lecture Notes in Computer Science, Springer Berlin Heidelberg (2007),http://link.springer.com/chapter...

    2007

  45. [54]

    In: Gopalakrishnan, G., Qadeer, S

    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification. pp. 585–591. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2011)

    2011

  46. [55]

    In: Proc

    Kurakin, A., Goodfellow, I.J., Bengio, S.: Adversarial examples in the physical world. In: Proc. of ICLR 2016 (Feb 2017),https://openreview.net/forum?id= HJGU3Rodl

    2016

  47. [56]

    In: Proceedings of the 16th international conference on Tools and Algorithms for the Construction and Analysis of Systems

    Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-Guarantee verification for probabilistic systems. In: Proceedings of the 16th international conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 23–37. TACAS’10, Springer-Verlag, Paphos, Cy...

    2010

  48. [57]

    Information and Computation 232, 38–65 (Nov 2013)

    Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Information and Computation 232, 38–65 (Nov 2013)

    2013

  49. [58]

    Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Model Checking and Autonomy. Annual Review of Control, Robotics, and Autonomous Systems5(1), 385–410 (2022).https://doi.org/10.1146/annurev-control-042820-010947, https://doi.org/10.1146/annurev-control-042820-010947, _epr...

    2022 doi

  50. [59]

    In: International Conference on Software Engineering and Formal Methods

    Legay, A., Sedwards, S., Traonouez, L.M.: Scalable verification of markov deci- sion processes. In: International Conference on Software Engineering and Formal Methods. pp. 350–362. Springer (2014)

    2014

  51. [60]

    Li,J.,Nuzzo,P.,Sangiovanni-Vincentelli,A.,Xi,Y.,Li,D.:Stochasticcontractsfor cyber-physical system design under probabilistic requirements. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for SystemDesign.pp.5–14.MEMOCODE’17,Associati...

    2017

  52. [61]

    In: Annals of Computer Science and Information Systems

    Kwiatkowska, M., Zhang, X.: When to Trust AI: Advances and Challenges for Certification of Neural Networks. In: Annals of Computer Science and Information Systems. vol. 35, pp. 25–37 (2023),https://annals-csis.org/Volume_35/drp/ 2324.html, iSSN: 2300-5963

    2023

  53. [62]

    In: Amato, N.M., Hager, G., Thomas, S., 26 Jordan Peper, Yan Miao, Sayan Mitra, and Ivan Ruchkin Torres-Torriti, M

    Liebenwein, L., Schwarting, W., Vasile, C.I., DeCastro, J., Alonso-Mora, J., Karaman, S., Rus, D.: Compositional and Contract-Based Verification for Au- tonomous Driving on Road Networks. In: Amato, N.M., Hager, G., Thomas, S., 26 Jordan Peper, Yan Miao, Sayan Mitra, and Ivan ...

    2020 doi

  54. [63]

    In: Proceedings of the 18th International Con- ference on Autonomous Agents and MultiAgent Systems

    Lomuscio, A., Pirovano, E.: A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems. In: Proceedings of the 18th International Con- ference on Autonomous Agents and MultiAgent Systems. pp. 161–169. AAMAS ’19, International Foundation for Autonomous ...

    2019

  55. [64]

    In: In Pro- ceedings of Learning for Decision and Control (L4DC) (2025)

    Li, Y., Ji, C., Anchalia, J., Mitra, S.: Lyapunov perception contracts. In: In Pro- ceedings of Learning for Decision and Control (L4DC) (2025)

    2025

  56. [65]

    IEEE Transactions on Automatic Control64(6), 2629– 2636 (2018), publisher: IEEE

    Mallik, K., Schmuck, A.K., Soudjani, S., Majumdar, R.: Compositional synthesis of finite-state abstractions. IEEE Transactions on Automatic Control64(6), 2629– 2636 (2018), publisher: IEEE

    2018

  57. [66]

    Miao, Y., Shen, W., Cui, H., Mitra, S.: Falconwing: An open-source platform for ultra-light fixed-wing aircraft research (2025),https://arxiv.org/abs/2505. 01383

    2025

  58. [67]

    https://doi.org/10.1007/978-3-030-28619-4_10

    Majumdar, A., Pavone, M.: How Should a Robot Assess Risk? Towards an Ax- iomaticTheoryofRiskinRobotics.In:RoboticsResearch.pp.75–84.SpringerPro- ceedings in Advanced Robotics, Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-28619-4_10

    2020 doi

  59. [68]

    Mildenhall, B., Srinivasan, P.P., Tancik, M., Barron, J.T., Ramamoorthi, R., Ng, R.: Nerf: representing scenes as neural radiance fields for view synthesis. Commun. ACM65(1), 99–106 (Dec 2021).https://doi.org/10.1145/3503250,https:// doi.org/10.1145/3503250

    2021 doi

  60. [69]

    Mitra, S., Păsăreanu, C., Prabhakar, P., Seshia, S.A., Mangal, R., Li, Y., Watson, C., Gopinath, D., Yu, H.: Formal Verification Techniques for Vision-Based Au- tonomous Systems – A Survey. In: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C.,Noll,T.,Quatmann,T.,Stoelinga,M...

    2025

  61. [70]

    In: IEEE/RSJ International Conference on Intelligent Robots and Systems

    Miao, Y., Shen, W., Mitra, S.: Zero-shot sim-to-real visual quadrotor control with hard constraints. In: IEEE/RSJ International Conference on Intelligent Robots and Systems. Hangzhou, China (October 2025)

    2025

  62. [71]

    In: 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)

    Naik, N., Nuzzo, P.: Robustness Contracts for Scalable Verification of Neural Network-Enabled Cyber-Physical Systems. In: 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). pp. 1–12 (Dec 2020).https://doi.org/10.1109/MEMOCODE...

    2020

  63. [72]

    Statistics in Medicine17(8), 857–872 (Apr 1998).https://doi.org/10.1002/(sici)1097-0258(19980430)17:8<857:: aid-sim777>3.0.co;2-e

    Newcombe, R.G.: Two-sided confidence intervals for the single propor- tion: comparison of seven methods. Statistics in Medicine17(8), 857–872 (Apr 1998).https://doi.org/10.1002/(sici)1097-0258(19980430)17:8<857:: aid-sim777>3.0.co;2-e

    1998 doi

  64. [73]

    In: Conference proceedings of the 2023 AIAA AVIATION Forum (May 2023).https://doi.org/10.48550/arXiv.2305.02449, http://arxiv.org/abs/2305.02449, arXiv:2305.02449 [cs, stat]

    Moss, R.J., Kochenderfer, M.J., Gariel, M., Dubois, A.: Bayesian Safety Val- idation for Black-Box Systems. In: Conference proceedings of the 2023 AIAA AVIATION Forum (May 2023).https://doi.org/10.48550/arXiv.2305.02449, http://arxiv.org/abs/2305.02449, arXiv:2305.02449 [cs, stat]

    2023 doi arXiv

  65. [74]

    ACM Transactions on Embedded Computing Systems18(1), 2:1–2:26 (Jan 2019).https://doi.org/10

    Nuzzo, P., Li, J., Sangiovanni-Vincentelli, A.L., Xi, Y., Li, D.: Stochastic Assume- Guarantee Contracts for Cyber-Physical System Design. ACM Transactions on Embedded Computing Systems18(1), 2:1–2:26 (Jan 2019).https://doi.org/10. 1145/3243216,https://doi.org/10.1145/3243216

    2019 doi

  66. [75]

    Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-Time VerificationofPCTLPropertiesofMDPswithConvexUncertainties.In:Computer Aided Verification. pp. 527–542. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2013).https://doi.org/10.1...

    2013 doi

  67. [76]

    In: Proceedings of the 2019 Inter- national Symposium on Physical Design

    Nuzzo, P.: From Electronic Design Automation to Cyber-Physical System Design Automation: A Tale of Platforms and Contracts. In: Proceedings of the 2019 Inter- national Symposium on Physical Design. pp. 117–121. ISPD ’19, Association for Computing Machinery, San Francisco, CA, ...

    2019

  68. [77]

    IEEE Tran

    Ruchkin, I., Sokolsky, O., Weimer, J., Hedaoo, T., Lee, I.: Compositional Prob- abilistic Analysis of Temporal Properties Over Stochastic Detectors. IEEE Tran. on Computer-Aided Design of Integrated Circuits and Systems39(11), 3288–3299 (Nov 2020).https://doi.org/10.1109/TCAD....

    2020

  69. [78]

    PhD Thesis, Carnegie Mellon University (Mar 2019),https://doi.org/10.1184/R1/ 7970222.v1

    Ruchkin, I.: Integration of Modeling Methods for Cyber-Physical Systems. PhD Thesis, Carnegie Mellon University (Mar 2019),https://doi.org/10.1184/R1/ 7970222.v1

    2019 doi

  70. [79]

    In: Computer Aided Verification

    Păsăreanu, C.S., Mangal, R., Gopinath, D., Getir Yaman, S., Imrie, C., Calinescu, R., Yu, H.: Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study. In: Computer Aided Verification. pp. 289–303. Lecture Notes in Computer Science, Springer Nature Switzerland, Ch...

    2023

  71. [80]

    In: 5th Analytic Virtual Integration of Cyber-Physical Systems Workshop

    Ruchkin, I., de Niz, D., Chaki, S., Garlan, D.: ACTIVE: A Tool for Integrating Analysis Contracts. In: 5th Analytic Virtual Integration of Cyber-Physical Systems Workshop. Rome, Italy (Dec 2014)

    2014

  72. [81]

    In: Proc

    Ruchkin, I., de Niz, D., Chaki, S., Garlan, D.: Contract-based Integration of Cyber- physical Analyses. In: Proc. of the Intl. Conf. on Embedded Software (EMSOFT). ACM, New York, NY, USA (2014).https://doi.org/10.1145/2656045.2656052

    2014

  73. [82]

    In: ACM/IEEE 13th Intl

    Ruchkin, I., Cleaveland, M., Ivanov, R., Lu, P., Carpenter, T., Sokolsky, O., Lee, I.: Confidence Composition for Monitors of Verification Assumptions. In: ACM/IEEE 13th Intl. Conf. on Cyber-Physical Systems (ICCPS). pp. 1–12 (May 2022).https: //doi.org/10.1109/ICCPS54341.2022.00007

    2022

  74. [83]

    Frankenstein: Contract-Based Design for Cyber-Physical Systems

    Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems. European Journal of Control 18(3), 217–238 (2012).https://doi.org/10.3166/ejc.18.217-238

    2012 doi

  75. [84]

    In: Deshmukh, J.V., Havelund, K., Perez, I

    Santa Cruz, U., Shoukry, Y.: NNLander-VeriF: A Neural Network Formal Verifi- cation Framework for Vision-Based Autonomous Aircraft Landing. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods. pp. 213–230. Lecture Notes in Computer Science, Springer Internat...

    2022

  76. [85]

    In: Arbab, F., Ölveczky, P.C

    Rushby, J.: Composing Safe Systems. In: Arbab, F., Ölveczky, P.C. (eds.) Formal Aspects of Component Software, pp. 3–11. No. 7253 in Lecture Notes in Com- puter Science, Springer Berlin Heidelberg (Jan 2012),http://link.springer. com/chapter/10.1007/978-3-642-35743-5_2

    2012 doi

  77. [86]

    In: 2024 IEEE International Conference on Robotics and Automation (ICRA)

    Sun, D., Yang, B.C., Mitra, S.: Learning-based inverse perception contracts and applications. In: 2024 IEEE International Conference on Robotics and Automation (ICRA). pp. 11612–11618 (2024).https://doi.org/10.1109/ICRA57147.2024. 10610329 28 Jordan Peper, Yan Miao, Sayan Mitr...

    2024

  78. [87]

    In: International Conference on Learning Representations (2014)

    Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks. In: International Conference on Learning Representations (2014)

    2014

  79. [88]

    In: 2018 17th IEEE International Conference on Machine Learning and Applications (ICMLA)

    Shvets, A.A., Rakhlin, A., Kalinin, A.A., Iglovikov, V.I.: Automatic Instrument Segmentation in Robot-Assisted Surgery using Deep Learning. In: 2018 17th IEEE International Conference on Machine Learning and Applications (ICMLA). pp. 624–628 (Dec 2018).https://doi.org/10.1109/...

    2018

  80. [89]

    In: Pro- ceedings of the eighth international symposium on imprecise probability : theories and applications

    Troffaes, M.C.M., Skulj, D.: Model checking for imprecise Markov chains. In: Pro- ceedings of the eighth international symposium on imprecise probability : theories and applications. pp. 337–344. Society for Imprecise Probability: Theories and Applications (SIPTA), Compiegne, ...

    2013

  81. [90]

    arXiv:1903.09354 [cs] (Mar 2019),http://arxiv.org/abs/ 1903.09354, arXiv: 1903.09354

    Vazquez-Chanlatte, M., Rabe, M.N., Seshia, S.A.: A Model Counter’s Guide to Probabilistic Systems. arXiv:1903.09354 [cs] (Mar 2019),http://arxiv.org/abs/ 1903.09354, arXiv: 1903.09354

    1903 arXiv

  82. [91]

    In: Proceedings of the Twelveth Interna- tional Symposium on Imprecise Probability: Theories and Applications

    Termine, A., Antonucci, A., Facchini, A., Primiero, G.: Robust Model Checking with Imprecise Markov Reward Models. In: Proceedings of the Twelveth Interna- tional Symposium on Imprecise Probability: Theories and Applications. pp. 299–

  83. [92]

    In: 2021 Design, Automation & Test in Europe Conference & Exhibition (DATE)

    Wang, Z., Huang, C., Wang, Y., Hobbs, C., Chakraborty, S., Zhu, Q.: Bounding Perception Neural Network Uncertainty for Safe Control of Autonomous Systems. In: 2021 Design, Automation & Test in Europe Conference & Exhibition (DATE). pp.1745–1750(Feb2021).https://doi.org/10.2391...

    2021

  84. [93]

    In: 2012 IEEE 51st IEEE Conference on Decision and Control (CDC)

    Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain Markov De- cision Processes with temporal logic specifications. In: 2012 IEEE 51st IEEE Conference on Decision and Control (CDC). pp. 3372–3379 (Dec 2012).https: //doi.org/10.1109/CDC.2012.6426174, iSSN: 0743-1546

    2012

  85. [94]

    2023 IEEE Conference on Secure and Trustworthy Ma- chine Learning (SaTML) pp

    Wu, H., Tagomori, T., Robey, A., Yang, F., Matni, N., Pappas, G., Hassani, H., Pasareanu, C., Barrett, C.: Toward Certified Robustness Against Real-World Distribution Shifts. 2023 IEEE Conference on Secure and Trustworthy Ma- chine Learning (SaTML) pp. 537–553 (Feb 2023).https...

    2023

  86. [95]

    Waite, T., Geng, Y., Turnquist, T., Ruchkin, I., Ivanov, R.: State-Dependent Con- formal Perception Bounds for Neuro-Symbolic Verification of Autonomous Systems (Feb 2025).https://doi.org/10.48550/arXiv.2502.21308,http://arxiv.org/ abs/2502.21308, arXiv:2502.21308 [eess]

    2025 doi arXiv

  87. [96]

    CVPR (2025)

    Xie, Z., Liu, Z., Peng, Z., Wu, W., Zhou, B.: Vid2sim: Realistic and interactive simulation from video for urban navigation. CVPR (2025)

    2025

  88. [97]

    arXiv preprint arXiv:2504.13175 (2025)

    Yang, S., Yu, W., Zeng, J., Lv, J., Ren, K., Lu, C., Lin, D., Pang, J.: Novel demon- stration generation with gaussian splatting enables robust one-shot manipulation. arXiv preprint arXiv:2504.13175 (2025)

    2025 arXiv

  89. [98]

    Zhao, X., Gerasimou, S., Calinescu, R., Imrie, C., Robu, V., Flynn, D.: Bayesian learning for the robust verification of autonomous robots. Communications Engi- neering3(1), 1–14 (Jan 2024).https://doi.org/10.1038/s44172-024-00162-y, Towards Unified Probabilistic Verification ...

    2024 doi

  90. [99]

    org/abs/2305.03882, arXiv:2305.03882 [cs]

    Xie, X., Song, J., Zhou, Z., Zhang, F., Ma, L.: Mosaic: Model-based Safety Analysis Framework for AI-enabled Cyber-Physical Systems (May 2023),http://arxiv. org/abs/2305.03882, arXiv:2305.03882 [cs]

    2023 arXiv

  91. [154]

    20 in Embedded Systems, Springer New York (2014)

    No. 20 in Embedded Systems, Springer New York (2014)

    2014

  92. [309]

    html, iSSN: 2640-3498

    PMLR (Aug 2021),https://proceedings.mlr.press/v147/termine21a. html, iSSN: 2640-3498

    2021

  93. [521]

    Springer Berlin Heidelberg (2011)

    2011

Pith tools

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