Skip to content


Repository files navigation

EMME: ECMAScript Memory Model Evaluator

This tools provides a SAT/SMT-based verification for JavaScript programs with shared array memory access (i.e., SharedArrayBuffer).

Learn more.

Briefly, given a JavaScript-like SharedArrayBuffer bounded execution program (see .bex files in the examples folder), EMME computes all valid executions according with the ECMA specification ( The valid executions are provided as: 1) a set of graphviz files represeting the memory model relations (i.e., mm*.dot), and 2) an assertion on the automatically generated JavaScript program (i.e., program.js).


Using Docker:

  1. install Docker with your package manager e.g., sudo apt-get install docker
  2. build the Docker image: cd docker/fedora_64 && docker build -f fedora-emme .
  3. run the Docker image: docker run -i -t fedora-emme /bin/bash

On Linux and MacOS:

  1. install python package dependencies: pip install -r requirements.txt
  2. install CVC4 SMT solver (see for licensing and additional informations): cd ext_tools && bash && cd ..
  3. install V8 JS engine (see for licensing and additional informations): cd ext_tools && bash && cd ..


To start playing with the tool, you can run:

  1. python examples/single_var/sv_simple01.bex (to generate the valid executions in the folder examples/single_var/sv_simple01/)
  2. python -c "bash ext_tools/" -i examples/single_var/sv_simple01/program.js -n 1k -j 4 (to check if the d8 engine obeys the expected results)
  3. python examples/single_var/sv_simple01.bex --unmatched --jsengine="bash ext_tools/" -n 1k -j 4 (to perform the behavioral coverage constraint analysis)
  4. python examples/single_var/sv_simple01.bex --synth (to generate all equivalent programs in the folder examples/single_var/sv_simple01/)

For more details on the license, have a look at LICENSE.txt


  • "EMME: a formal tool for ECMAScript Memory Model Evaluation". C. Mattarei, C. Barrett, S. Guo, B. Nelson, and B. Smith. TACAS 2018, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Thessaloniki (Greece).

Build Status

Code Health