Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Narrowing by fixed number of meets #1494

Open
1 task
sim642 opened this issue May 29, 2024 · 0 comments
Open
1 task

Narrowing by fixed number of meets #1494

sim642 opened this issue May 29, 2024 · 0 comments
Labels
feature good first issue precision relational Relational analyses (Apron, affeq, lin2var)

Comments

@sim642
Copy link
Member

sim642 commented May 29, 2024

Based on the delayed widening from #1483, we could easily implement a domain lifter for narrowing that applies meet at most a fixed number of times. This makes it possible to have a terminating narrow for domains that do not have narrowings. It is a standard technique.

Our current analysis for the polyhedral example that #1484 is fixing is even more imprecise than the old literature suggests. This is because Apron doesn't provide narrowing for polyhedra and thus we cannot make any decreasing iterations. But the standard implementation of narrowing for polyhedra is to do a fixed number of meets.

@sim642 sim642 added feature precision good first issue relational Relational analyses (Apron, affeq, lin2var) labels May 29, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature good first issue precision relational Relational analyses (Apron, affeq, lin2var)
Projects
None yet
Development

No branches or pull requests

1 participant