Proving programs robust

By Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman, S. Navidpour. 2011

141 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Software

Citations in the corpus

Minimax Rates of Estimating Approximate Differential Privacy (2019, methodology): “acy loss of a software program that uses multiple dierentially private accesses to the data, including SQL-based languages [McS09], higher-order functional languages [RP10], and imperative languages [CGLN11]. A 3 unifying recipe of these approaches is to combine standard mechanisms like Laplacian, e”
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018, methodology): “[28] considered a definition of robustness that is similar to the one in our work, and [5] used a combination of abstract interpretation and SMT-based methods to prove robustness of programs.”
Verified Computational Differential Privacy with Applications to Smart Metering (2013, methodology): “Another challenge is to provide tool-support for reasoning about the utility of differentially private algorithms, which would require more advanced methods to derive bounds about the probability of events w.r.t. distributions generated by programs (e.g. Chebyshev’s inequality).”
Probabilistic relational reasoning for differential privacy (2012, methodology): “In contrast to [9, 24, 29], CertiPriv supports reasoning about differential privacy guarantees from first principles.”
Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs (2013, methodology): “Moreover, several language-based methods have been developed for guaranteeing differential privacy; these methods are based on runtime verification, such as PINQ [21] or Airavat [28], type systems [26, 18], or deductive verification [10].”
Robustness Analysis of Finite Precision Implementations (2013, unknown): “This is illustrated on the left-hand side of Figure 2, on which we represented the zonotopic abstractions r̂ [3] and r̂ z [5]: it clearly appears that the zonotopic abstraction is not sufficient to accurately bound the discontinuity error (in the ellipse), that will locally involve some interval-lik”
Approximate Computing: A Survey (2016, background): “These analyses reason about programs 1) that operate on approximate hardware [34], 2) are transformed using accuracy-aware transformations [26], and 3) operate on uncertain inputs [38].”
Managing performance vs. accuracy trade-offs with loop perforation (2011, background): “An extension of this research introduces a notion of function robustness, and, under an input locality condition, presents an approximate memoization approach similar to loop perforation [11].”
Differential Privacy by Typing in Security Protocols (2013, background): “[33] have introduced a generic robustness property for programs that encompasses sensitivity and can be statically enforced even for programs featuring complex branching structures and loops.”