Software

During the course of research, we have developed and released the following software and datasets.

Trustworthy and Deployable Machine Learning

• VarDetect: Stateful detection of model extraction attacks

  • For technical details, see this technical report.

• ActiveThief: Model extraction using active learning and unannotated public data

  • For technical details, see our AAAI'20 paper.

Machine Learning for Software Engieering

• CuBERT: Code understanding BERT

  • For technical details, see our ICML'20 paper.

• ETHPy150Open dataset: A redistributable subset of the ETH Py150 corpus

  • For technical details, see our ICML'20 paper.

• NBL: Neural-attribution for semantic bug localization

  • For technical details, see our NeurIPS'19 paper.

• RLAssist: Deep reinforcement learning for syntactic error repair

  • For technical details, see our AAAI'19 paper.

• Bandit AFL: Greybox fuzzing as a contextual bandits problem

  • For technical details, see the technical report.

• DeepFix: Fixing common C language errors by deep learning

  • For technical details, see our AAAI'17 paper.

• CoderAssist: Semi-supervised verified feedback generation for programming assignments

  • For technical details, see our FSE'16 paper.

• MintHint: Automated synthesis of repair hints

  • For technical details, see our ICSE'14 paper.

• MathFinder: Math API discovery and migration

  • For technical details, see our FASE'13 and TOSEM'14 papers.

Concurrency and Distribution

• EventTrack: Efficient computation of happens-before relation for event-driven programs

  • For technical details, see our ISSTA'17 paper.

• DeadWait: Static deadlock detection for asynchronous C# programs

  • For technical details, see our PLDI'17 paper.

  • DeadWait found several new deadlock conditions in open-source and industrial libraries. A total of 40 of them have been fixed after we reported them. See this page for more details.

• SparseRacer: Efficient race detection for programmatic event loops

  • For technical details, see our ISSTA'16 paper.

  • SparseRacer found several new bugs in real applications, several of which have been confirmed and even fixed by the developers. See this page for more details.

• EM-Explorer: A proof-of-concept stateless model checker for concurrent Android applications

  • For technical details, see our TACAS'16 paper.

• DroidRacer: Dynamic race detection for Android applications

  • For technical details, see our PLDI'14 paper.

Program Analysis and Verification

• Symbolic simulation and test generation for Matlab Simulink/Stateflow

  • For technical details, see our EMSOFT'08 and CAV'09 papers.

• SPOTS: A system for proving optimizing transformations sound

  • For technical details, see our SEFM'06, ENTCS'07 and SPE'09 papers.