Arrow Research search

Author name cluster

Corina Pasareanu

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

TMLR Journal 2022 Journal Article

Degradation Attacks on Certifiably Robust Neural Networks

  • Klas Leino
  • Chi Zhang
  • Ravi Mangal
  • Matt Fredrikson
  • Bryan Parno
  • Corina Pasareanu

Certifiably robust neural networks protect against adversarial examples by employing run-time defenses that check if the model is certifiably locally robust at the input under evaluation. We show through examples and experiments that any defense (whether complete or incomplete) based on checking local robustness is inherently over-cautious. Specifically, such defenses flag inputs for which local robustness checks fail, but yet that are not adversarial; i.e., they are classified consistently with all valid inputs within a distance of $\epsilon$. As a result, while a norm-bounded adversary cannot change the classification of an input, it can use norm-bounded changes to degrade the utility of certifiably robust networks by forcing them to reject otherwise correctly classifiable inputs. We empirically demonstrate the efficacy of such attacks against state-of-the-art certifiable defenses. Our code is available at https://github.com/ravimangal/degradation-attacks.

TCS Journal 2005 Journal Article

Combining test case generation and runtime verification

  • Cyrille Artho
  • Howard Barringer
  • Allen Goldberg
  • Klaus Havelund
  • Sarfraz Khurshid
  • Mike Lowry
  • Corina Pasareanu
  • Grigore Roşu

Software testing is typically an ad hoc process where human testers manually write test inputs and descriptions of expected test results, perhaps automating their execution in a regression suite. This process is cumbersome and costly. This paper reports results on a framework to further automate this process. The framework consists of combining automated test case generation based on systematically exploring the input domain of the program with runtime verification, where execution traces are monitored and verified against properties expressed in temporal logic. Capabilities also exist for analyzing traces for concurrency errors, such as deadlocks and data races. The input domain of the program is explored using a model checker extended with symbolic execution. Properties are formulated in an expressive temporal logic. A methodology is advocated that automatically generates properties specific to each input rather than formulating properties uniformly true for all inputs. The paper describes an application of the technology to a NASA rover controller.

v2026.09.13