-
Using a Driver’s Eye Information to Determine Drowsiness
- Organized and implemented a user study to test whether or not eye information can be used to determine a person’s drowsiness levels. Results showed a strong correlation of eye information and drowsiness level, but not high predictive value.
- Dataset Webpage
-
Formal Expression and Verification of Recursive Symbolic Execution
- Formally expressed and verified structural properties of a system that utilizes a recursive version of symbolic execution to verify hardware security in Coq.
- Github Repository
-
Using Model Checking to Find Safety-Critical Ambiguities in Adaptive Cruise Control System Specifications
- Utilized multiple model checking tools to find 6 major ambiguities in the International Organization of Standardization’s specification of an adaptive cruise control system.
-
Formally Verifying the Fundamental Properties of Symbolic Execution
- Formally expressed and verified the fundamental properties of symbolic execution in Dafny.
- Github Repository