diff --git a/_posts/2016-07-07-jstools.md b/_posts/2016-07-07-jstools.md new file mode 100644 index 0000000000000000000000000000000000000000..54fdb718ca5c75310bbb6e8c0e7874489fdf2c12 --- /dev/null +++ b/_posts/2016-07-07-jstools.md @@ -0,0 +1,17 @@ +--- +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. \ No newline at end of file