Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • verified-software/publications
1 result
Show changes
Commits on Source (1)
Hide whitespace changes
Inline Side-by-side
Showing
with 16 additions and 1 deletion
publications.bib
View file @ da9c1f7f
......@@ -1434,7 +1434,7 @@ Firefox test suite which illustrate the scoping mechanism of
the JavaScript variable store.},
file = {:Gardner2013JuS.pdf:PDF},
}
@article{DBLP:journals/pacmpl/SantosMNWG18,
@article{Fragoso2018JaVerT,
author = {Jos{\'{e}} Fragoso Santos and
Petar Maksimovic and
Daiva Naudziuniene and
......@@ -1446,6 +1446,21 @@ the JavaScript variable store.},
number = {{POPL}},
pages = {50:1--50:33},
year = {2018},
abstract = {The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification.
We introduce JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich,
mechanically verified specifications of critical JavaScript code. To specify JavaScript programs,
we design abstractions that capture its key heap structures (for example, prototype chains and function closures),
allowing the developer to write clear and succinct specifications with minimal knowledge of the JavaScript internals.
To verify JavaScript programs, we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL,
a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript;
JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic;
and verified axiomatic specifications of the JavaScript internal functions.
Using JaVerT, we verify functional correctness properties of:
data-structure libraries (key-value map, priority queue) written in an object-oriented style;
operations on data structures such as binary search trees (BSTs) and lists; examples illustrating function closures;
and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger,
more complex code using JaVerT is feasible.
},
url = {http://doi.acm.org/10.1145/3158138},
doi = {10.1145/3158138},
timestamp = {Fri, 05 Jan 2018 12:57:30 +0100},
......