Portus: Linking Alloy with SMT-based Finite Model Finding
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912932858691584 |
|---|---|
| author | Dancy, Ryan Day, Nancy A. Zila, Owen Tariq, Khadija Poremba, Joseph |
| author_facet | Dancy, Ryan Day, Nancy A. Zila, Owen Tariq, Khadija Poremba, Joseph |
| contents | Alloy is a well-known, formal, declarative language for modelling systems early in the software development process. Currently, it uses the Kodkod library as a back-end for finite model finding. Kodkod translates the model to a SAT problem; however, this method can often handle only problems of fairly low-size sets and is inherently finite. We present Portus, a method for translating Alloy into an equivalent many-sorted first-order logic problem (MSFOL). Once in MSFOL, the problem can be evaluated by an SMT-based finite model finding method implemented in the Fortress library, creating an alternative back-end for the Alloy Analyzer. Fortress converts the MSFOL finite model finding problem into the logic of uninterpreted functions with equality (EUF), a decidable fragment of first-order logic that is well-supported in many SMT solvers. We compare the performance of Portus with Kodkod on a corpus of 63 Alloy models written by experts. Our method is fully integrated into the Alloy Analyzer. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_15978 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Portus: Linking Alloy with SMT-based Finite Model Finding Dancy, Ryan Day, Nancy A. Zila, Owen Tariq, Khadija Poremba, Joseph Software Engineering Logic in Computer Science Alloy is a well-known, formal, declarative language for modelling systems early in the software development process. Currently, it uses the Kodkod library as a back-end for finite model finding. Kodkod translates the model to a SAT problem; however, this method can often handle only problems of fairly low-size sets and is inherently finite. We present Portus, a method for translating Alloy into an equivalent many-sorted first-order logic problem (MSFOL). Once in MSFOL, the problem can be evaluated by an SMT-based finite model finding method implemented in the Fortress library, creating an alternative back-end for the Alloy Analyzer. Fortress converts the MSFOL finite model finding problem into the logic of uninterpreted functions with equality (EUF), a decidable fragment of first-order logic that is well-supported in many SMT solvers. We compare the performance of Portus with Kodkod on a corpus of 63 Alloy models written by experts. Our method is fully integrated into the Alloy Analyzer. |
| title | Portus: Linking Alloy with SMT-based Finite Model Finding |
| topic | Software Engineering Logic in Computer Science |
| url | https://arxiv.org/abs/2411.15978 |