[{"_1":2,"_152":-5,"_153":-5},"loaderData",{"_3":4,"_13":14,"_20":21,"_131":132},"root",{"_5":-5,"_6":-7,"_7":8,"_9":-7,"_10":11,"_12":-7},"currentUser","primaryEmail","siteVerification","6LeIxAcTAAAAAJcZVRqyHh71UMIEGNQ_MXjiZKhI","toast","enableDev",false,"incidentStatus","routes/_layout",{"_15":-5,"_16":17,"_18":17,"_19":11},"username","isAskGordonEnabled",true,"isUsingNewTemplate","showMinimalLanding","routes/_layout.r.$namespace.$reponame",{"_22":23,"_24":-5,"_25":11,"_26":11,"_27":28,"_29":30,"_31":-5,"_32":11,"_33":34,"_83":-5,"_84":85,"_124":-5,"_125":11,"_126":17,"_127":11,"_128":-5,"_129":130},"canonicalUrl","https://hub.docker.com/r/padhi/loopinvgen/tags","mcpServer","canSeeDockerfile","canSeeAutobuilds","namespace","padhi","reponame","loopinvgen","cloudBuildSource","isAutobuildsAvailable","repo",{"_35":36,"_37":38,"_40":41,"_42":43,"_44":11,"_45":46,"_47":48,"_49":50,"_52":30,"_27":28,"_53":54,"_55":39,"_56":57,"_58":59,"_60":61,"_62":-5,"_63":57,"_64":65,"_66":11,"_67":28,"_68":69,"_74":11,"_75":76,"_80":28,"_81":82},"categories",[],"content_types",[39],"image","date_registered","2019-03-04T10:02:35.027112Z","description","A data-driven tool that generates provably sufficient loop invariants for program verification.","is_private","last_updated","2020-04-23T13:58:01.242714Z","last_modified","2024-10-16T13:48:34.145251Z","media_types",[51],"application/vnd.docker.container.image.v1+json","name","pull_count",570,"repository_type","star_count",0,"status",1,"status_description","active","source","collaborator_count","full_description","LoopInvGen\n

\n==========\n\n[![](https://img.shields.io/travis/SaswatPadhi/LoopInvGen/master.svg?logo=travis&style=popout&label=Travis+Build)][travis]\n \n[![](https://img.shields.io/docker/cloud/build/padhi/loopinvgen.svg?logo=docker&style=popout&label=Docker+Image)][docker-hub]\n\nA data-driven tool that generates provably sufficient loop invariants for program verification.\n\n

\n \n
\n _{\n [ LoopInvGen extends our old (now deactivated) project, PIE -- the Precondition Inference Engine. ]\n}\n

\n\n\n---\n\n[**Installation**](#installation)\n | \n[Invariant Inference](#invariant-inference)\n · \n[Batch Verification](#batch-verification)\n | \n[_Use as a Library_](app/)\n | \n[Citing LoopInvGen](#citing-loopinvgen)\n · \n[License (MIT)](LICENSE.md)\n\n---\n\n#### :page_with_curl: Papers and Presentations\n\n- [CAV 2019](http://i-cav.org/2019) --\n Paper on the [_Hybrid Enumeration_ (HEnum)](https://saswatpadhi.github.io/assets/pdf/cav2019_overfitting.pdf) technique used for \"feature\" synthesis within LoopInvGen\n- [PLDI 2016](http://conf.researchr.org/home/pldi-2016) --\n Original paper on the [_Precondition Inference Engine_ (PIE)](https://saswatpadhi.github.io/assets/pdf/pldi2016_pie.pdf), the backbone of LoopInvGen\n

\n- [SyGuS-Comp 2019] (in conjunction with CAV and SYNT 2019) --\n Solver [Presentation](docs/2019_SyGuS-Comp-Presentation.pdf) and [Description](docs/2019_SyGuS-Comp-Description.pdf)\n- [SyGuS-Comp 2018] (a satellite event of CAV and SYNT at FLoC 2018) --\n Solver [Presentation](docs/2018_SyGuS-Comp-Presentation.pdf) and [Description](docs/2018_SyGuS-Comp-Description.pdf)\n- [SyGuS-Comp 2017] (in conjunction with CAV and SYNT 2017) --\n Solver [Presentation](docs/2017_SyGuS-Comp-Presentation.pdf) and [Description](docs/2017_SyGuS-Comp-Description.pdf)\n\n#### :trophy: Awards and Honors\n\n- [SyGuS-Comp 2018] -- Inv Track **Winner** ([Results](https://sygus.org/comp/2018/results-slides.pdf) and [Report](https://sygus.org/comp/2018/report.pdf))\n- [SyGuS-Comp 2017] -- Inv Track **Winner** ([Results](https://sygus.org/comp/2017/results-slides.pdf) and [Report](https://sygus.org/comp/2017/report.pdf))\n\n## Installation\n\n### Using `docker` (recommended)\n\n_**Note:** The docker image may consume ~ 3 GB of disk space._\n\nWe recommend running LoopInvGen within a docker container,\nsince they have negligible performance overhead.\n(See [this report](http://domino.research.ibm.com/library/cyberdig.nsf/papers/0929052195DD819C85257D2300681E7B/$File/rc25482.pdf))\n\n0. [Get `docker` for your OS](https://docs.docker.com/install).\n1. Pull our docker image^[#](#note_1): `docker pull padhi/loopinvgen`.\n2. Run a container over the image: `docker run -it padhi/loopinvgen`.
\n This would give you a `bash` shell within LoopInvGen directory.\n\n^# Alternatively, you could also build the Docker image locally:\n\n```bash\ndocker build -t padhi/loopinvgen github.com/SaswatPadhi/LoopInvGen\n```\n\nDocker containers are isolated from the host system.\nTherefore, to run LoopInvGen on SyGuS files residing on the host system,\nyou must first [bind mount] them while running the container:\n\n```bash\ndocker run -v /host/dir:/home/opam/LoopInvGen/shared -it padhi/loopinvgen\n```\n\nThe `/host/dir` on the host system would then be accessible within the container at `~/LoopInvGen/shared` (with read+write permissions).\n\n

\n\n

Docker also allows you to easily limit the container's memory and/or CPU usage.

\n\n```bash\n# Create a LoopInvGen container with 4GB memory, no swap and 1 CPU\n$ docker run -it --memory=4g --memory-swap=4g --cpus=1 padhi/loopinvgen\n```\n\nSee [the official Docker guide](https://docs.docker.com/config/containers/resource_constraints)\nfor more details on applying resource constraints.\n\n

\n\n\n### Manual Installation\n\n

\n\n

CLICK to reveal instructions

\n\n#### 0. Get the required packages for your OS.\n\nPlease see the [`Dockerfile`](Dockerfile#L19-L21) for the complete list of required packages\nfor building LoopInvGen and its dependencies. \nMost of these packages are already installed on standard installations of most *nix distributions,\nexcept, may be, these: `aspcud libgmp-dev libomp-dev m4`.\n\n#### 1. Install `opam` package manager for OCaml.\n\nSee for detailed instructions.\n\n#### 2. Install `ocaml` >= 4.08.0.\nWe recommend using an OCaml compiler with [`flambda`][flambda] optimizations enabled.\nFor example, with [opam](https://opam.ocaml.org/) 2.0+, you could run `opam switch create 4.10.0+flambda`.\n\n#### 3. `opam install` the dependencies.\n```bash\n$ opam install alcotest.1.1.0 core.v0.13.0 dune.2.5.1\n```\n\n#### 4. Get the [Z3 project][z3].\nWe have tested LoopInvGen with the latest stable version of Z3 (4.8.7).\nYou could either:\n- `git checkout https://github.com/Z3Prover/z3.git` for the bleeding-edge version, or\n- `wget https://github.com/Z3Prover/z3/archive/z3-4.8.7.zip && unzip z3-4.8.7.zip` for the stable version\n\n#### 5. `git clone` this project, and build everything.\n```bash\n$ ./scripts/build_all.sh -z /PATH/TO/z3_dir\n```\nThe `build_all.sh` script would build Z3, copy it to `_dep/`, and then build LoopInvGen.\nAlternatively, you can copy a precompiled version of Z3 to a `_dep` directory at the root of the repository,\nand simply run `./scripts/build_all.sh`.\n\nFor debug builds, use the `-D` or `--debug` switch when invoking `build_all.sh`.\n\nFor future builds after any changes to the source code, you only need to run `dune build`.\nYou can configure the build profile to either `debug` or `optimize` (default),\nusing: `dune build --profile `. \n\n

\n\n## Invariant Inference\n\nInfer invariants for SyGuS-INV benchmarks by invoking LoopInvGen as:\n```bash\n$ ./loopinvgen.sh benchmarks/LIA/2016.SyGuS-Comp/array.sl\n(define-fun inv-f ((x Int) (y Int) (z Int)) Bool (not (and (>= x 5) (not (<= y z)))))\n```\n\n**Note:** LoopInvGen processes benchmarks in multiple stages.\nWe trap CTRL+C (`SIGINT` signal) to break out of the current stage,\nand CTRL+\\\\ (`SIGQUIT` signal) to kill LoopInvGen and with its child processes.\n\n#### Inference Timeout\n\nYou may use the `-t` flag to run LoopInvGen with a maximum limit\non the number of _seconds_ (wall-clock time) for which the inference algorithm may run.\n```bash\n$ ./loopinvgen.sh -t 8 benchmarks/LIA/2016.SyGuS-Comp/array.sl\n```\n\nFor timeout based on CPU time, you may use [`ulimit`](https://ss64.com/bash/ulimit.html).\n\n#### Manually Adding Features\n\nYou may use the `-F` flag to preseed LoopInvGen's inference engine\nwith custom features (written in SMTLib format).\n```bash\n$ ./loopinvgen.sh -F benchmarks/NIA/2018.CHI_InvGame/~features/s10.some.smt2.input benchmarks/NIA/2018.CHI_InvGame/s10.desugared.sl\n```\n\n

\n\n

CLICK for further details

\n\n#### Verifying Generated Invariants\n\nThe `-v` switch makes LoopInvGen verify the benchmark with the generated invariant:\n```bash\n$ ./loopinvgen.sh -v benchmarks/LIA/2016.SyGuS-Comp/array.sl\nPASS\n```\n\nIt gives one of the following verdicts:\n```\nPASS : The generated invariant successfully verifies the benchmark.\nPASS (NO SOLUTION) : The benchmark is invalid (no invariant can verify it),\n and no invariant was generated.\nFAIL {;...} : The generated invariant fails to verify the VCs: vc1, vc2 etc.\n where each VC is one of {pre, post, trans}.\nFAIL (NO SOLUTION) : The benchmark is invalid (no invariant can verify it),\n but an invariant (that is not empty/false) was generated.\n[TIMEOUT] : Invariant inference timed out.\n With an empty (false) invariant, is one of the verdicts above.\n```\n\nTry `./loopinvgen.sh -h` for other options that allow more control over the inference process.\n\n

\n\n\n## Batch Verification\n\nExecute `./scripts/test_all.sh -b benchmarks/LIA` to run LoopInvGen on all benchmarks in [benchmarks/LIA].\nThe `test_all.sh` script invokes LoopInvGen for invariant inference,\nand then verifies that the generated invariant is sufficient to prove correctness of the SyGuS benchmark.\n\n**Note:** Within `test_all.sh`,\nwe trap CTRL+C (`SIGINT` signal) to kill the currently running benchmark,\nand CTRL+\\\\ (`SIGQUIT` signal) to kill the `test_all.sh` script with its child processes.\n\n

\n\n

CLICK for further details

\n\nFor each benchmark, the `test_all.sh` script generates one of the verdicts mentioned [above](#verifying-generated-invariants), or:\n```\n[SKIPPED] : Invariant inference was skipped for an already passing benchmark.\n is one of the PASS verdicts above.\n```\n\n#### Rerunning Failed Benchmarks\n\nThe `test_all.sh` script creates a new log directory and tests all benchmarks each time it is run.\nHowever, one may want to rerun only the previously failed benchmarks, for example with a different timeout,\nfrom a previously failing run.\nThis can be achieved by forcing `test_all.sh` to use a previous log directory, using `-l `.\n\n#### Benchmarking with Other Inference Tools\n\n`test_all.sh` is a generic benchmarking script that may run any invariant inference tool\nwhich accepts the SyGuS format. This makes it easier for us to compare various tools easily. \nTo use an invariant inference tool other than LoopInvGen, invoke it as:\n```bash\n$ ./scripts/test_all.sh -b -T [-- [-tool] [-specific] [-options]]\n```\n\n#### Limiting Execution Time\n\nJust like `loopinvgen.sh`, the `test_all.sh` script allows users to limit the\nexecution time for the invariant inference tools using the `-t` flag.\n```bash\n$ ./scripts/test_all.sh -b benchmarks/LIA -t 10\n```\n\nTry `./scripts/test_all.sh -h` for more options.\n\n

\n\n## Citing LoopInvGen\n\n```\n@inproceedings{pldi/2016/PadhiSM,\n author = {Saswat Padhi and Rahul Sharma and Todd D. Millstein},\n title = {Data-Driven Precondition Inference with Learned Features},\n booktitle = {Proceedings of the 37th {ACM} {SIGPLAN} Conference on Programming\n Language Design and Implementation, {PLDI} 2016, Santa Barbara, CA,\n USA, June 13-17, 2016},\n pages = {42--56},\n year = {2016},\n url = {http://doi.acm.org/10.1145/2908080.2908099},\n doi = {10.1145/2908080.2908099}\n}\n```\n\n[benchmarks/LIA]: benchmarks/LIA\n\n[flambda]: https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html\n[bind mount]: https://docs.docker.com/storage/bind-mounts\n\n[SyGuS-Comp 2017]: https://sygus.org/comp/2017\n[SyGuS-Comp 2018]: https://sygus.org/comp/2018\n[SyGuS-Comp 2019]: https://sygus.org/comp/2019\n\n[docker-hub]: https://hub.docker.com/r/padhi/loopinvgen\n[travis]: https://travis-ci.org/SaswatPadhi/LoopInvGen\n[z3]: https://github.com/Z3Prover/z3","has_starred","hub_user","immutable_tags_settings",{"_70":11,"_71":72},"enabled","rules",[73],".*","is_automated","permissions",{"_77":17,"_78":11,"_79":11},"read","write","admin","user","storage_size",14553843690,"orgData","recentTags",[86],{"_87":39,"_88":89,"_90":91,"_92":93,"_94":95,"_45":113,"_114":89,"_115":28,"_116":51,"_52":117,"_118":119,"_120":104,"_121":113,"_122":61,"_123":17},"content_type","creator",3348487,"full_size",853076372,"id",48597822,"images",[96],{"_97":98,"_99":100,"_101":102,"_103":104,"_105":106,"_107":108,"_109":102,"_110":-5,"_111":91,"_58":61,"_112":-5},"architecture","amd64","digest","sha256:78d7562a022972973975d969d824175737ca0285c771b3ad23212cb11cfd5dc0","features","","last_pulled","2026-09-16T20:49:40.446196327Z","last_pushed","2020-04-23T13:58:01Z","os","linux","os_features","os_version","size","variant","2020-04-23T13:58:00.807688Z","last_updater","last_updater_username","media_type","latest","repository",6772145,"tag_last_pulled","tag_last_pushed","tag_status","v2","sbxKitMetadata","isPotentialSpam","isHubSbxKitsEnabled","displaySecurityMetadata","tagAttestations","tagsHaveAttestations",[],"routes/_layout.r.$namespace.$reponame.tags",{"_33":133,"_140":141,"_129":150,"_151":11},{"_35":134,"_37":135,"_40":41,"_42":43,"_44":11,"_45":46,"_47":48,"_49":136,"_52":30,"_27":28,"_53":54,"_55":39,"_56":57,"_58":59,"_60":61,"_62":-5,"_63":57,"_64":65,"_66":11,"_67":28,"_68":137,"_74":11,"_75":139,"_80":28,"_81":82},[],[39],[51],{"_70":11,"_71":138},[73],{"_77":17,"_78":11,"_79":11},"tags",{"_142":59,"_143":-5,"_144":-5,"_145":146},"count","next","previous","results",[147],{"_87":39,"_88":89,"_90":91,"_92":93,"_94":148,"_45":113,"_114":89,"_115":28,"_116":51,"_52":117,"_118":119,"_120":104,"_121":113,"_122":61,"_123":17},[149],{"_97":98,"_99":100,"_101":102,"_103":104,"_105":106,"_107":108,"_109":102,"_110":-5,"_111":91,"_58":61,"_112":-5},[],"canDeleteTags","actionData","errors"]

padhi/loopinvgen

Tags for padhi/loopinvgen