[{"_1":2,"_176":-5,"_177":-5},"loaderData",{"_3":4,"_17":18,"_25":26,"_151":152},"root",{"_5":-5,"_6":-7,"_7":8,"_9":-7,"_10":11,"_12":-7,"_13":14,"_15":16},"currentUser","primaryEmail","siteVerification","6LeIxAcTAAAAAJcZVRqyHh71UMIEGNQ_MXjiZKhI","toast","enableDev",false,"incidentStatus","theme","system","contrast","normal","routes/_layout",{"_19":-5,"_20":21,"_22":21,"_23":11,"_24":21},"username","isAskGordonEnabled",true,"isUsingNewTemplate","showMinimalLanding","showHoneypotTrap","routes/_layout.r.$namespace.$reponame",{"_27":28,"_29":-5,"_30":11,"_31":11,"_32":33,"_34":35,"_36":-5,"_37":11,"_38":39,"_88":-5,"_89":90,"_140":-5,"_141":11,"_142":21,"_143":11,"_144":-5,"_145":11,"_146":-5,"_147":148,"_149":91,"_150":-7},"canonicalUrl","https://hub.docker.com/r/parfdocker/parf-jcst/tags","mcpServer","canSeeDockerfile","canSeeAutobuilds","namespace","parfdocker","reponame","parf-jcst","cloudBuildSource","isAutobuildsAvailable","repo",{"_40":41,"_42":43,"_45":46,"_47":48,"_49":11,"_50":51,"_52":53,"_54":55,"_57":35,"_32":33,"_58":59,"_60":44,"_61":62,"_63":64,"_65":66,"_67":-5,"_68":62,"_69":70,"_71":11,"_72":33,"_73":74,"_79":11,"_80":81,"_85":33,"_86":87},"categories",[],"content_types",[44],"image","date_registered","2024-12-27T03:59:27.498835Z","description","","is_private","last_updated","2025-03-19T13:16:48.731638Z","last_modified","2025-03-19T13:19:06.640297Z","media_types",[56],"application/vnd.docker.container.image.v1+json","name","pull_count",149,"repository_type","star_count",0,"status",1,"status_description","active","source","collaborator_count","full_description","# Description of docker image for experiments reproduction\n\n# Parf: An Adaptive Abstraction-Strategy Tuner for Static Analysis\n\nParf is a toolkit for adaptively tuning abstraction strategies of static program analyzers in a fully automated manner. This repository contains a Docker image of Parf (as a plugin to Frama-C) used to replicate the experimental results reported in the paper titled \"Parf: An Adaptive Abstraction-Strategy Tuner for Static Analysis\" submitted to JCST.\n\n## Set up\n\n1. Install Docker as per .\n\n2. Pull Parf from dockerhub:\n\n ```shell\n docker pull parfdocker/parf-jcst:v2.0\n ```\n\n To check whether you have successfully pulled the correct docker image: run `docker images` and see if `parfdocker/parf-jcst` exists.\n\n3. Run the Docker container:\n\n ```shell\n docker run -it parfdocker/parf-jcst:v2.0\n ```\n\n You should be in a terminal environment as the root. Then\n\n ```shell\n root@300735229ca6:~# ls\n Parf-Benchmark\n ```\n\n4. Synchronize the environment with the current opam switch in the container:\n\n ```\n eval $(opam env)\n ```\n\n5. Check whether `Frama-C` and `Parf` is available in the container:\n\n ```\n frama-c --version\n ```\n\n and\n\n ```\n frama-c -parf-h\n ```\n\n\n\n## Usage\n\n```\nframa-c -parf [OPTION]\n```\n\nBelow are the most commonly used external options for Parf, along with their default values:\n\n+ `-parf-budget`: Specifies the total time budget (in seconds) for the entire Parf analysis. Default value: `300`.\n+ `-parf-process`: Determines the number of processes used for parallel computation. Set to `0` for sequential computation (default value).\n+ `-parf-sample-num`: Defines the number of samples per refinement iteration. Default value: `4`.\n\nWe recommend setting the value of `-parf-sample-num` to be 1–2 times the value of `-parf-process` for optimal performance. Here are some examples of using Parf:\n\n+ Analyze `oscs-benchmarks/2048/2048.c` using the sequential version of Parf with a 300-second time budget:\n\n ```\n frama-c oscs-benchmarks/2048/2048.c -parf -parf-budget 300\n ```\n\n+ Analyze `oscs-benchmarks/2048/2048.c` using the parallel version of Parf with 4 processes and a 300-second time budget, generating 8 samples in each iteration:\n\n ```\n frama-c oscs-benchmarks/2048/2048.c -parf -parf-budget 300 -parf-process 4 -parf-sample-num 8\n ```\n\n\n\n## Reproduction of Experiments in the Paper\n\n### RQ1: Consistency with [ASE '24](https://doi.org/10.1145/3691620.3695487)\n\n#### Check the experimental results in submitted paper\n\n1. Run `cd ~/Parf-Benchmark/scripts `\n\n2. Check the summaries of experimental results of the `Parf` tool and the other four baselines:\n\n + `Parf_Opt`: `cat log_parf-optimum.txt`\n + `Parf_Avg`: `cat log_parf-server1-summary.txt log_parf-server2-summary.txt log_parf-server3-summary.txt ` (The `Parf_Avg` in RQ1 lists the average #alarms of three independent experiments' results)\n + `-eva-precision 0`: `cat log_eva_precision0-summary.txt`\n + `Default`: `cat log_eva_default-summary.txt`.\n + `Official`: `cat log_eva_official-summary.txt`.\n + `Expert`: `cat log_eva_expert-summary.txt`.\n\n The results of each benchmark are in the form of:\n\n ```\n , Alarms: , Time: , Parameters: \n ```\n\n where ``, `num_of_alarms`, `time`, and `final_parameters` are respectively the name of the benchmark, the number of alarms reported by the final analysis, the analysis time, and the parameter setting of the final analysis (for `log_parf-server1-summary.txt`, `log_parf-server2-summary.txt`, `log_parf-server3-summary.txt`, and `log_eva_precision0-summary.txt`).\n\n3. Check the detailed log of each analysis for a certain benchmark (e.g., ``), of `Parf` and other four baselines:\n\n + `Parf`: `cat ../oscs-benchmarks//.frama-c/log_parf-server1`, `cat ../oscs-benchmarks//.frama-c/log_parf-server2`, and `cat ../oscs-benchmarks//.frama-c/log_parf-server3`. For example, `cat ../oscs-benchmarks/2048/.frama-c/log_parf-server1` for benchmark `2048`.\n + `-eva-precision 0`: `cat ../oscs-benchmarks//.frama-c/log_eva_precision0`\n + `Default`: `cat ../oscs-benchmarks//.frama-c/log_eva_default-server`\n + `Official`: `cat ../oscs-benchmarks//.frama-c/log_eva_official-server`\n + `Expert`: `cat ../oscs-benchmarks//.frama-c/log_eva_expert-server`\n Note that many analysis logs of`Expert` baseline do not end with a `Frama-C/Eva` summary, i.e. the final analysis interrupts due to the time limit, so you may have to manually search the last completed analysis.\n\n#### To reproduce the experimental results\n\n1. Run `cd ~/Parf-Benchmark/scripts`.\n\n2. Reproduce the results.\n\n + `-eva-precision 0`:\n\n ```\n ./run_oscs_eva_precision0.sh --logfile=log_eva_precision0-reproduce\n python3 summarize.py log_eva_precision0-reproduce ../oscs-benchmarks\n ```\n\n The generated summary file is `log_eva_precision0-reproduce-summary.txt`.\n\n + `Default`:\n\n ```\n ./run_oscs_eva_default.sh --logfile=log_eva_default-reproduce\n python3 summarize.py log_eva_default-reproduce ../oscs-benchmarks\n ```\n\n The generated summary file is `log_eva_default-reproduce-summary.txt`.\n\n + `Expert`: (it is expected to take more than 20 hours)\n\n ```\n ./run_oscs_eva_expert.sh --logfile=log_eva_expert-reproduce\n python3 summarize.py log_eva_expert-reproduce ../oscs-benchmarks\n ```\n\n The generated summary file is `log_eva_expert-reproduce-summary.txt`.\n\n + `Official`:\n\n ```\n ./run_oscs_eva_official.sh log_eva_official-reproduce\n python3 summarize.py log_eva_official-reproduce ../oscs-benchmarks\n ```\n\n The generated summary file is `log_eva_official-reproduce-summary.txt`.\n\n + `Parf`:\n\n Given the inherent randomness of Parf, we conduct 3-repeated experiments under the same hyper-parameter configurations with [ASE '24](https://doi.org/10.1145/3691620.3695487) (it is expected to take more than 20 hours for each experiment):\n\n ```\n ./run_oscs_parf.sh --timeBudget=3600 --processCore=4 --sampleNum=4 --refineNum=7 --logFile=log_parf-reproduce1 --output=.parf_log-reproduce1\n python3 summarize.py log_parf-reproduce1 ../oscs-benchmarks\n ```\n\n ```\n ./run_oscs_parf.sh --timeBudget=3600 --processCore=4 --sampleNum=4 --refineNum=7 --logFile=log_parf-reproduce2 --output=.parf_log-reproduce2\n python3 summarize.py log_parf-reproduce2 ../oscs-benchmarks\n ```\n\n ```\n ./run_oscs_parf.sh --timeBudget=3600 --processCore=4 --sampleNum=4 --refineNum=7 --logFile=log_parf-reproduce3 --output=.parf_log-reproduce3\n python3 summarize.py log_parf-reproduce3 ../oscs-benchmarks\n ```\n\n The generated summary files for each experiments are `log_parf-reproduce1-summary.txt`, `log_parf-reproduce2-summary.txt`, and `log_parf-reproduce3-summary.txt`.\n\n Then identify the optimal outcome (output as `log_parf-optimum-reproduce.txt`) by:\n\n ```\n python3 collect_best_analysis.py log_parf-reproduce1-summary.txt log_parf-reproduce2-summary.txt log_parf-reproduce3-summary.txt --output_file=log_parf-optimum-reproduce.txt\n ```\n\n### RQ2: Dominancy\n\n#### Check the experimental results in submitted paper\n\n1. Run `cd ~/Parf-Benchmark/scripts`.\n\n2. Run `cat dominant_params/summary_table_precision0.csv `\n\n The format is as follows:\n\n ```csv\n Project,Analysis,Alarms,Time\n monocypher,selected-10.log,606,3:03.01\n monocypher,remaining-8.log,574,16:16.82\n monocypher,selected-12.log,606,3:02.45\n monocypher,selected-1.log,601,4:08.90\n ...\n ```\n\n Each row represents the result of a controlled experiment.\n\n Notably, a controlled experiment somehow does not terminate in the 30-minute time budget, for example:\n\n ```\n kilo,selected-5.log,N/A,30:00.04\n ```\n\n Then we treat this experiment by setting its reported alarms same as the `-eva-precision 0` baseline.\n\n#### To reproduce the experimental results\n\n1. Partition the parameter settings for 13 pairs of controlled experiments for each benchmark:\n\n ```shell\n python3 partition_parameters.py log_parf-optimum-reproduce.txt dominant_params-reproduce\n ```\n\n Note: if you replace the `log_parf-optimum-reproduce.txt` with `log_parf-optimum.txt`, you will reproduce the exactly same results displayed in the submitted paper.\n\n2. Conduct the controlled experiments (it is expected to take more than 10 hours):\n\n ```\n python3 conduct_dominant_experiments.py --parameters_dir dominant_params-reproduce --projects_dir ../oscs-benchmarks\n ```\n\n3. Collect the results of all controlled experiments:\n\n ```sh\n python3 summarize_dominant.py ../oscs-benchmarks dominant_params-reproduce\n ```\n\n Then check the results: `cat dominant_params-reproduce/summary_table_precision0.csv`.\n\n### RQ3: Interpretability\n\nThe source program of RQ3 is the `2018_06_parser/parser_full.c` of the benchmark `tutorials`: `cat ~/Parf-Benchmark/oscs-benchmarks/tutorials/2018_06_parser/parser_full.c`.\n\n1. Run `cd ~/Parf-Benchmark/oscs-benchmarks/tutorials/2018_06_parser/`.\n\n2. To reproduce the analysis result of `Expert`:\n\n ```\n frama-c parser_full.c -eva -eva-precision 11\n ```\n\n , which is same as\n\n ```\n frama-c parser_full.c -eva -eva-widening-delay 6 -eva-subdivide-non-linear 220 -eva-split-return auto -eva-slevel 5000 -eva-remove-redundant-alarms -eva-plevel 2000 -eva-partition-history 2 -eva-octagon-through-calls -eva-min-loop-unroll 4 -eva-ilevel 256 -eva-equality-through-calls formals -eva-domains cvalue,equality,gauges,octagon,symbolic-locations -eva-auto-loop-unroll 1024\n ```\n\n The result summary is\n\n ```\n [eva:summary] ====== ANALYSIS SUMMARY ======\n ----------------------------------------------------------------------------\n 5 functions analyzed (out of 7): 71% coverage.\n In these functions, 89 statements reached (out of 89): 100% coverage.\n ----------------------------------------------------------------------------\n No errors or warnings raised during the analysis.\n ----------------------------------------------------------------------------\n 1 alarm generated by the analysis:\n 1 access out of bounds index\n ----------------------------------------------------------------------------\n Evaluation of the logical properties reached by the analysis:\n Assertions 3 valid 2 unknown 0 invalid 5 total\n Preconditions 7 valid 1 unknown 0 invalid 8 total\n 76% of the logical properties reached have been proven.\n ----------------------------------------------------------------------------\n ```\n\n If you replace the `-eva-partition-history 2` in the above parameter setting with `-eva-partition-history 0` used by `Expert`, the false alarm will be eliminated:\n\n ```\n frama-c parser_full.c -eva -eva-widening-delay 6 -eva-subdivide-non-linear 220 -eva-split-return auto -eva-slevel 5000 -eva-remove-redundant-alarms -eva-plevel 2000 -eva-partition-history 0 -eva-octagon-through-calls -eva-min-loop-unroll 4 -eva-ilevel 256 -eva-equality-through-calls formals -eva-domains cvalue,equality,gauges,octagon,symbolic-locations -eva-auto-loop-unroll 1024\n ```\n\n3. To reproduce the analysis result of `Parf`:\n\n ```\n frama-c parser_full.c -eva -eva-widening-delay 21 -eva-subdivide-non-linear 391 -eva-split-return auto -eva-slevel 5866 -eva-remove-redundant-alarms -eva-plevel 4001 -eva-partition-history 0 -eva-octagon-through-calls -eva-min-loop-unroll 0 -eva-ilevel 513 -eva-equality-through-calls formals -eva-domains cvalue,equality,gauges,octagon,symbolic-locations -eva-auto-loop-unroll 1651\n ```\n\n The result summary is\n\n ```\n [eva:summary] ====== ANALYSIS SUMMARY ======\n ----------------------------------------------------------------------------\n 5 functions analyzed (out of 7): 71% coverage.\n In these functions, 89 statements reached (out of 89): 100% coverage.\n ----------------------------------------------------------------------------\n No errors or warnings raised during the analysis.\n ----------------------------------------------------------------------------\n 0 alarms generated by the analysis.\n ----------------------------------------------------------------------------\n Evaluation of the logical properties reached by the analysis:\n Assertions 3 valid 2 unknown 0 invalid 5 total\n Preconditions 8 valid 0 unknown 0 invalid 8 total\n 84% of the logical properties reached have been proven.\n ----------------------------------------------------------------------------\n ```\n\n If you replace the `-eva-partition-history 0` in the above parameter setting used by `Parf` with `-eva-partition-history 2`, the false alarm will be reported:\n\n ```\n frama-c parser_full.c -eva -eva-widening-delay 21 -eva-subdivide-non-linear 391 -eva-split-return auto -eva-slevel 5866 -eva-remove-redundant-alarms -eva-plevel 4001 -eva-partition-history 2 -eva-octagon-through-calls -eva-min-loop-unroll 0 -eva-ilevel 513 -eva-equality-through-calls formals -eva-domains cvalue,equality,gauges,octagon,symbolic-locations -eva-auto-loop-unroll 1651\n ```","has_starred","hub_user","immutable_tags_settings",{"_75":11,"_76":77},"enabled","rules",[78],".*","is_automated","permissions",{"_82":21,"_83":11,"_84":11},"read","write","admin","user","storage_size",3566515228,"orgData","recentTags",[91,128],{"_92":44,"_93":94,"_95":96,"_97":98,"_99":100,"_101":102,"_50":117,"_118":94,"_119":33,"_120":56,"_57":121,"_122":123,"_124":108,"_125":117,"_126":66,"_127":21},"content_type","creator",28234552,"digest","sha256:6dcf2c32566437bf328dcbca76592d39c86734b094c84d5c75bcd51f88275d85","full_size",1731947457,"id",867111170,"images",[103],{"_104":105,"_95":96,"_106":48,"_107":108,"_109":110,"_111":112,"_113":48,"_114":-5,"_115":98,"_63":66,"_116":-5},"architecture","amd64","features","last_pulled","2026-09-23T02:23:48.603239473Z","last_pushed","2025-03-19T13:16:47.255804723Z","os","linux","os_features","os_version","size","variant","2025-03-19T13:16:47.659029Z","last_updater","last_updater_username","media_type","v2.0","repository",26053688,"tag_last_pulled","tag_last_pushed","tag_status","v2",{"_92":44,"_93":94,"_95":129,"_97":130,"_99":131,"_101":132,"_50":138,"_118":94,"_119":33,"_120":56,"_57":139,"_122":123,"_124":135,"_125":138,"_126":66,"_127":21},"sha256:839c5fbc9c2d968286fa96477d92f520873632ad8b3a0eb1d35a6bf337800e8d",1834549001,820982423,[133],{"_104":134,"_95":129,"_106":48,"_107":135,"_109":136,"_111":112,"_113":48,"_114":-5,"_115":130,"_63":66,"_116":137},"arm64","2026-09-25T08:12:24.820702746Z","2024-12-30T02:35:40Z","v8","2024-12-30T02:35:39.519201Z","v1.0","sbxKitMetadata","isPotentialSpam","isHubSbxKitsEnabled","showSbxLogoOverride","sbxTrademarkText","displaySecurityMetadata","tagAttestations","tagsHaveAttestations",[],"selectedTag","attestationsUrl","routes/_layout.r.$namespace.$reponame.tags",{"_38":153,"_160":161,"_147":174,"_175":11},{"_40":154,"_42":155,"_45":46,"_47":48,"_49":11,"_50":51,"_52":53,"_54":156,"_57":35,"_32":33,"_58":59,"_60":44,"_61":62,"_63":64,"_65":66,"_67":-5,"_68":62,"_69":70,"_71":11,"_72":33,"_73":157,"_79":11,"_80":159,"_85":33,"_86":87},[],[44],[56],{"_75":11,"_76":158},[78],{"_82":21,"_83":11,"_84":11},"tags",{"_162":163,"_164":-5,"_165":-5,"_166":167},"count",2,"next","previous","results",[168,171],{"_92":44,"_93":94,"_95":96,"_97":98,"_99":100,"_101":169,"_50":117,"_118":94,"_119":33,"_120":56,"_57":121,"_122":123,"_124":108,"_125":117,"_126":66,"_127":21},[170],{"_104":105,"_95":96,"_106":48,"_107":108,"_109":110,"_111":112,"_113":48,"_114":-5,"_115":98,"_63":66,"_116":-5},{"_92":44,"_93":94,"_95":129,"_97":130,"_99":131,"_101":172,"_50":138,"_118":94,"_119":33,"_120":56,"_57":139,"_122":123,"_124":135,"_125":138,"_126":66,"_127":21},[173],{"_104":134,"_95":129,"_106":48,"_107":135,"_109":136,"_111":112,"_113":48,"_114":-5,"_115":130,"_63":66,"_116":137},[],"canDeleteTags","actionData","errors"]

parfdocker/parf-jcst

Tags for parfdocker/parf-jcst