Show simple item record

dc.contributor.authorPoremba, Joseph
dc.contributor.authorDay, Nancy A.
dc.contributor.authorVakili, Amirhossein
dc.date.accessioned2023-07-24 14:00:46 (GMT)
dc.date.available2023-07-24 14:00:46 (GMT)
dc.date.issued2023-06-01
dc.identifier.urihttps://doi.org/10.1109/TSE.2023.3256939
dc.identifier.urihttp://hdl.handle.net/10012/19627
dc.description© 2023 IEEE. J. Poremba, N. A. Day and A. Vakili, "New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding," in IEEE Transactions on Software Engineering, vol. 49, no. 6, pp. 3487-3503, 1 June 2023, doi: 10.1109/TSE.2023.3256939.en
dc.description.abstractSymmetry in finite model finding problems of many-sorted first-order logic (MSFOL) can be exploited to reduce the number of interpretations considered during search, thereby improving solver performance for tools such as the Alloy Analyzer. We present a framework to soundly compose static symmetry breaking schemes for MSFOL: 1) one for functions with distinct sorts in the domain and range; 2) one for functions where the range sort appears in the domain; and 3) one for predicates. We provide a novel presentation of sort inference in the context of symmetry breaking that yields a new mathematical link between sorts and symmetries. We empirically investigate how our symmetry breaking approaches affect solving performance.en
dc.description.sponsorshipThis work was supported in part by the Natural Sciences and Engineering Research Council of Canada (NSERC).en
dc.language.isoenen
dc.publisherIEEEen
dc.relation.ispartofseriesIEEE Transactions on Software Engineering;
dc.subjectfinite model findingen
dc.subjectsymmetry breakingen
dc.titleNew Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Findingen
dc.typeArticleen
dcterms.bibliographicCitationJ. Poremba, N. A. Day and A. Vakili, "New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding," in IEEE Transactions on Software Engineering, vol. 49, no. 6, pp. 3487-3503, 1 June 2023, doi: 10.1109/TSE.2023.3256939.en
uws.contributor.affiliation1Faculty of Mathematicsen
uws.contributor.affiliation2David R. Cheriton School of Computer Scienceen
uws.typeOfResourceTexten
uws.peerReviewStatusRevieweden
uws.scholarLevelFacultyen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record


UWSpace

University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages