GitHub - jsl1994/Phocus: This repository provides the code for the paper "Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers". This code implements Phocus which synthesizes precise abstract transformers for 3 different finite difference schemes used to solve hyperbolic partial differential equations.

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 1 Commit
LICENSE.txt		LICENSE.txt
MixedAAIA.py		MixedAAIA.py
README.txt		README.txt
cfl_checks.py		cfl_checks.py
experiment.py		experiment.py
finite_difference_schemes.py		finite_difference_schemes.py
fluxes.py		fluxes.py
helpers.py		helpers.py
iterative_solver.py		iterative_solver.py
process_output.py		process_output.py
run_LWR.py		run_LWR.py
run_buckley_leverett.py		run_buckley_leverett.py
run_burgers.py		run_burgers.py
run_chezy.py		run_chezy.py
run_cubic_lax_fried.py		run_cubic_lax_fried.py
run_cubic_leapfrog.py		run_cubic_leapfrog.py
run_cubic_upwind.py		run_cubic_upwind.py
run_large_burgers.py		run_large_burgers.py
run_medium_burgers.py		run_medium_burgers.py
run_small_burgers.py		run_small_burgers.py
run_trilinear.py		run_trilinear.py

Repository files navigation

Enclosed in this zip file are all the scripts used to run our code artifact for the paper "Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers"

Documentation of this code is found in CodeDocumentation.pdf

Additional documentation describing which parts of the code were designed for reuse and how to extend them is provided in ReusabilityGuide.pdf

After installing all dependencies (described in CodeDocumentation.pdf) the experiments are run with the following commands:

python3 run_burgers.py
python3 run_trilinear.py
python3 run_LWR.py
...

The experiments will output a row of latex-formatted text that reproduces the rows of Table 1 of our paper. In addition, plots comprising the figures of our paper will also be output in folders.

About

This repository provides the code for the paper "Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers". This code implements Phocus which synthesizes precise abstract transformers for 3 different finite difference schemes used to solve hyperbolic partial differential equations.

Readme

View license