title:Demo on the use of JaVerT at the JSTools'17 workshop
---
José Fragoso Santos gave a talk and demo on the use of JaVerT at the [JSTools'17 workshop](http://2017.ecoop.org/track/JSTools-2017-papers#program),
part of this year’s European Conference on Object-Oriented Programming [(ECOOP 2017)](http://2017.ecoop.org)
The demo illustrated how JaVerT can be used to specify and verify a JavaScript priority queue implementation,
showcasing the abstractions provided by JaVerT for reasoning about the JavaScript semantics, with an emphasis on objects,
prototype chains, and function closures, as well as the infrastructure for supporting arbitrary user-defined recursive predicates.
JaVerT is a semi-automatic verification tool chain for JavaScript based on separation logic. It targets functionally correct specifications
of critical JavaScript software, in particular small Node.js libraries that have high usability: for example, those describing well-known data structures,
such as a priority queue. JaVerT provides a wide variety of built-in abstractions so that our specifications are straightforward,
despite the underlying complexity of the JavaScript semantics.
JSTools’s aim is to bring together participants from academia and industry working on the analysis of JavaScript and its dialects,
to share ideas and problems, with a focus on presentations of shareable infrastructure.
