polywit
🌍 A poly-language execution-based violation-witness validator
Science Score: 57.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
✓DOI references
Found 6 DOI reference(s) in README -
○Academic publication links
-
○Committers with academic emails
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (12.6%) to scientific vocabulary
Keywords
Repository
🌍 A poly-language execution-based violation-witness validator
Basic Info
Statistics
- Stars: 4
- Watchers: 1
- Forks: 0
- Open Issues: 8
- Releases: 4
Topics
Metadata Files
README.md
Description
Modern verification tools report a violation witness amidst verification if a bug is encountered. Polywit employs execution-based validation to check the validity of the counterexample. This process involves extracting information on the assumptions of the verifier from the standardized exchange format for violation witnesses and building a test harness to provide a concrete execution of the program. The tool then executes the test harness on the code under verification and can either confirm or reject the violation witness if the relevant assertion is reached.
Whilst most modern execution-based validators such as wit4java and CPA-wit2test focus on specific language, polywit aims to provide an extensible, feature rich framework to allow for easy language integration and validator quality.
Framework
For a general language, the polywit implementation has the following architecture:
- The File Processor deals with processing of the compilation units.
- The Witness Processor deals with processing of the witness.
- The Test Harness deals with construction and execution of a test to check the validity of the reported violation.
Literature
- Wit4Java: A violation-witness validator for Java verifiers (competition contribution) by Wu, T., Schrammel, P., & Cordeiro, L. C. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Cham, 2022. Springer doi.org/10.1007/978-3-030-99527-0_36 ### Usage ``` usage: polywit [-h] frontend ...
Validate a given program with a witness conforming to the appropriate SV-COMP exchange format.
positional arguments: frontend Frontend language java Use the java validator
options: -h, --help show this help message and exit ```
Authors
Joss Moffatt (University of Manchester, United Kingdom) josshmoffatt@gmail.com
Tong Wu (University of Manchester, United Kingdom) wutonguom@gmail.com
Lucas Cordeiro (University of Manchester, United Kingdom) lucas.cordeiro@manchester.ac.uk
Peter Schrammel (University of Sussex, United Kingdom) P.Schrammel@sussex.ac.uk
Citation (CITATION.cff)
cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
- family-names: Moffatt
given-names: Joss
- family-names: Wu
given-names: Tong
orcid: https://orcid.org/0000-0002-0986-4150
- family-names: Cordeiro
given-names: Lucas
orcid: https://orcid.org/0000-0002-6235-4272
- family-names: Schrammel
given-names: Peter
orcid: https://orcid.org/0000-0002-5713-1381
title: "Polywit: The poly-language execution-based violation-witness validator"
license: MIT
license-url: "https://github.com/polywit/polywit/blob/main/LICENSE"
repository-code: "https://github.com/polywit/polywit"
type: software
version: 1.0.0
date-released: 2022
GitHub Events
Total
Last Year
Committers
Last synced: almost 3 years ago
All Time
- Total Commits: 61
- Total Committers: 2
- Avg Commits per committer: 30.5
- Development Distribution Score (DDS): 0.016
Top Committers
| Name | Commits | |
|---|---|---|
| Joss Moffatt | j****t@g****m | 60 |
| Merajul Arefin | m****n@g****m | 1 |
Issues and Pull Requests
Last synced: 6 months ago
All Time
- Total issues: 22
- Total pull requests: 12
- Average time to close issues: about 1 month
- Average time to close pull requests: 3 days
- Total issue authors: 1
- Total pull request authors: 2
- Average comments per issue: 0.23
- Average comments per pull request: 0.0
- Merged pull requests: 12
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 0
- Pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Issue authors: 0
- Pull request authors: 0
- Average comments per issue: 0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0
Top Authors
Issue Authors
- jossmoff (22)
Pull Request Authors
- jossmoff (11)
- j0ker70 (1)
Top Labels
Issue Labels
Pull Request Labels
Packages
- Total packages: 1
-
Total downloads:
- pypi 11 last-month
- Total dependent packages: 0
- Total dependent repositories: 0
- Total versions: 5
- Total maintainers: 1
pypi.org: polywit
A poly-language execution-based violation-witness validator.
- Homepage: https://github.com/polywit/polywit
- Documentation: https://polywit.readthedocs.io/
- License: mit
-
Latest release: 1.0.0
published over 3 years ago
Rankings
Maintainers (1)
Dependencies
- kentaro-m/auto-assign-action v1.2.4 composite
- actions/checkout v3 composite
- actions/setup-python v3 composite
- pypa/gh-action-pypi-publish 27b31702a0e7fc50959f5ad993c78deac1bdfc29 composite
- halo * development
- javalang * development
- kopyt * development
- networkx * development
- setuptools ==65.6.3 development
- tabulate * development