Formal Analysis of Perception Errors and Their System-level Effects_1

We are considering a system to produce alerts for runway incursions enabling safe landing of airplanes.
The system is implemented as an ML based object detector, followed by downstream conventional modules for tracking and alerting.

Goal: Investigate how imperfect ML perception affects system behavior guided by formal specifications.

Broad outline of steps:
1. Identify semantic conditions associated with perception errors (false and missed detections).
2. Formally guide system testing: Create diagnostic specifications (temporal and semantic) and test the detector–tracker–alert pipeline wrt the specifications.
3. Characterize and investigate system failures: Analyze violation traces and execution logs to mine recurring failure patterns and determine how perception errors propagate to system-level behavior.
4. The project will also investigate model-checking methods (time-permitting) to identify and characterize failures.

Desired Technical Qualifications:
1. Strong programming skills (Python and ML related packages).
2. Knowledge of Machine Learning: Deep Neural Networks , Vision models
3. Knowledge of Formal Methods would greatly help: Automata Theory, Formal temporal reasoning, Declarative languages, Model checking, SAT/SMT solving
4. Knowledge of Algorithms for Computer Vision is a bonus.
5. Knowledge of systems engineering (specifically aviation systems) is a bonus.

**Eligible Applicants:** Student
**Academic Level:** Undergraduate Senior, Graduate Master's, Graduate Doctoral, Post Doctoral
**Activity Type:** In-person
**Citizenship:** US Citizen Only
**Type:** Internships