Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2017-164

November 26, 2017

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-164.pdf

We consider the problem of performing compositional verification of a system with machine learning components whose behavior cannot easily be formally specified. We present an approach involving a system-level verifier communicating with a component-level analyzer wherein the former identifies a subset of environment behaviors that might lead to a system-level failure while the latter identifies erroneous behaviors, such as misclassifications, of the machine learning component that might be extended to a system-level counterexample. Results on cyber-physical systems with deep learning components used for perception demonstrate the promise of this approach.

---

BibTeX citation:

@techreport{Seshia:EECS-2017-164,
    Author= {Seshia, Sanjit A.},
    Title= {Compositional Verification without Compositional Specification for Learning-Based Systems},
    Year= {2017},
    Month= {Nov},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-164.html},
    Number= {UCB/EECS-2017-164},
    Abstract= {We consider the problem of performing compositional verification
of a system with machine learning components whose behavior
cannot easily be formally specified. 
We present an approach involving a system-level verifier
communicating with a component-level analyzer wherein 
the former identifies a subset of environment behaviors
that might lead to a system-level failure while the latter
identifies erroneous behaviors, such as misclassifications,
of the machine learning component that might be extended
to a system-level counterexample.
Results on cyber-physical systems with deep learning
components used for perception demonstrate the promise of
this approach.},
}

EndNote citation:

%0 Report
%A Seshia, Sanjit A. 
%T Compositional Verification without Compositional Specification for Learning-Based Systems
%I EECS Department, University of California, Berkeley
%D 2017
%8 November 26
%@ UCB/EECS-2017-164
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-164.html
%F Seshia:EECS-2017-164