is a separation-logic-based tool for JavaScript analysis and testing that follows
the language semantics without simplifications. It supports whole-program symbolic
testing, verification, and automatic compositional testing based on bi-abduction.
The award, one of five awarded on the call, was open to research teams working on
[applying formal methods using continuous reasoning and in particular, those addressing
fundamental problems for mostly-automatic or interactive verifiers.](https://research.fb.com/programs/research-awards/proposals/continuous-reasoning-research-award/)