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 characterize the topological structure of hyperproperties, design languages to specify them, and develop methods to verify them.
Quantitative properties assign numerical values to system executions, enabling reasoning about robustness, performance, and the severity of violations.
I establish classifications and hierarchies of quantitative properties and develop automata-theoretic 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
