RSS Meetups are monthly gatherings of LASIGE members with interests in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, Formal methods and other topics.

Title: JaVerT 2.0: Compositional Symbolic Execution for JavaScript

Presenter: José Fragoso Santos (Imperial College London)

Abstract: The dynamic nature of JavaScript and its complex semantics make it a difficult target for program analysis and verification. We will present JaVerT 2.0, a JavaScript Verification and Testing Toolchain that combines symbolic execution and compositional program reasoning based on separation logic.  JaVerT 2.0 supports scalable whole-program symbolic testing, full verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. We will give an overview of the architecture and metatheory of JaVerT 2.0 and illustrate how it can be used in the verification and testing of JavaScript programs, using the example of a simple expression evaluator. Further details can be found in the eponymous paper to be presented at POPL’19 and in the original JaVerT paper published in POPL’18. 

Short Bio: José Fragoso Santos completed his MSc in Information Systems and Computer Engineering at Instituto Superior Técnico and  his PhD in Computer Science at Inria Sophia Antipolis. During his PhD, he studied different types of information flow control mechanisms for securing client-side web applications. Currently, he is a post-doctoral researcher at Imperial College London, where he works with Philippa Gardner on the specification, verification, and testing of JavaScript programs. His latest work on JaVerT 2.0, a toolchain for JavaScript verification and testing, was given a Continuous Reasoning Research Award by Facebook.