Ana Jovanovic

dblp:272/7758 · DBLP profile ↗
← Back
3ranked-venue papers
3as first author
3since 2021 · last 2025
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 3 · 3 first-author · 3 since 2021
YearPublicationVenuePosition
2025 Mutation testing for temporal alloy models (extended version)
Ana Jovanovic, Allison Sullivan
Softw. Syst. Model.1
2024 Right or Wrong - Understanding How Users Write Software Models in Alloy
Ana Jovanovic, Allison Sullivan
SEFM1
2022 REACH: Refining Alloy Scenarios by Size (Tools and Artifact Track)
abstract
Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well suited for verifying system designs. A key strength of Alloy is its scenario-finding toolset, the Analyzer, which allows users to explore all valid scenarios that adhere to the model's constraints up to a user-provided scope. In Alloy, the Analyzer presents scenarios in the order they are discovered by a backend SAT solver, which is effectively unordered. This paper presents Reach, an enhancement to the Analyzer which allows users to explore scenarios by size. Experimental results reveal Reach's enumeration improves performance while having the added benefit of maintaining a semi-sorted ordering of scenarios for the user. Moreover, we highlight Reach's ability to improve the performance of Alloy's analysis when the user makes incremental changes to the scope.
Ana Jovanovic, Allison Sullivan
ISSRE1