Data

Tools

Indexes

Applications

Experiments

Open Source Science

pog2smtlib-2.7

Generates SMT-LIB 2.7 encodings for proof obligations from Atelier B.

https://github.com/CLEARSY/pog2smtlib-2.7

Science Score: 44.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
  • ○
    Academic publication links
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (7.1%) to scientific vocabulary
Last synced: 7 months ago · JSON representation ·

Repository

Generates SMT-LIB 2.7 encodings for proof obligations from Atelier B.

Basic Info
  • Host: GitHub
  • Owner: CLEARSY
  • License: gpl-3.0
  • Language: SMT
  • Default Branch: main
  • Homepage:
  • Size: 610 KB
Statistics
  • Stars: 0
  • Watchers: 2
  • Forks: 0
  • Open Issues: 3
  • Releases: 0
Created over 1 year ago · Last pushed 7 months ago
Metadata Files
Readme Contributing License Citation Cla

README.md

pog2smtlib-2.7

License

Build & Test Code format

pog2smtlib-2.7 is a translator from pog to SMT-LIB 2.7. It targets the HO-ALL logic and aims at supporting the full language of Atelier B proof obligations.

Usage

sh pog2smtlib27 -i <input.pog> -o <output>

Compilation

To compile the project with CMake: Oui, c'est l'outil pog2smtlib-2.7 sh cmake -B build cmake --build build

Testing

To test the project (after compilation), run the following commands:

sh cd build ctest

Contributing

We welcome external contributors to pog2smtlib-2.7!

Please carefully read the CONTRIBUTING.md file in this repository in case you consider contributing.

Licensing

This code is distributed under the license: "GNU GENERAL PUBLIC LICENSE, Version 3". See the LICENSE file in this repository.

Acknowledgments

This project is developed and maintained by CLEARSY. It has been partly financed by the Agence Nationale de la Recherche grant ANR-21-CE25-0010 for the BLaSST project (Enhancing B Language Reasoners with SAT and SMT Techniques).

Owner

  • Name: CLEARSY
  • Login: CLEARSY
  • Kind: organization
  • Email: contact@clearsy.com
  • Location: CLEARSY

CLEARSY Systems Engineering

Citation (CITATION.cff) 

cff-version: 1.2.0
title: pog2smtlib-2.7
message: >-
  If you use this software, please cite it using the metadata from this file.
type: software
authors:
  - name: CLEARSY
repository-code: "https://github.com/CLEARSY/pog2smtlib-2.7"
abstract: >
  Tool translating proof obligations from the POG format to SMT-LIB 2.7. The
  generated SMT-LIB problem includes the axiomatization of the B operators used
  in the proof obligation. The produced SMT-LIB problem is multi-sorted and
  monomorphization is applied to handle polymorphic operators such as ∈.
license: GPL-3.0

GitHub Events

Total
  • Delete event: 1
  • Push event: 9
  • Pull request event: 5
  • Create event: 3
Last Year
  • Delete event: 1
  • Push event: 9
  • Pull request event: 5
  • Create event: 3

Dependencies

.github/workflows/cmake-multi-platform.yml actions
  • actions/checkout v4 composite
  • jurplel/install-qt-action v4 composite
.github/workflows/clang-format-check.yml actions
  • RafikFarhad/clang-format-github-action v3 composite
  • actions/checkout v2 composite