I help people build dependable computer systems by developing theories and algorithms for formally specifying requirements and verifying systems against them.
Hyperproperties specify correct system implementations by describing how different executions relate, capturing information-flow properties, algorithmic fairness, counterfactual causality, and more.
I investigate how the structure of hyperproperties affects their verification and use this understanding to develop specification languages and verification techniques.
Quantitative properties assign numerical values to system executions, enabling reasoning about robustness, performance, and the severity of violations.
I study when and at what cost quantitative requirements can be verified automatically and develop algorithms and software for their analysis and verification.
Runtime monitoring observes system behavior during execution and assesses its correctness and performance against formal specifications.
I determine how resource constraints affect monitorability and develop sound approximation techniques to reduce monitors' resource use with a bounded loss of precision.
Quantitative Hyperproperties: Specification, Taxonomy, and Runtime Monitoring
QHyperSTAR brings these three research directions together. It lays the foundations of quantitative hyperproperties—specifications that map system implementations to numerical values by relating their executions—through a semantic classification, an expressive specification language, and memory-efficient monitoring algorithms.
CORDIS project record
