TACAS Conference 2026 Conference Paper
Syntactically Convex Model-Based Projection for Linear Real Arithmetic
- Anna Becchi
- Grigory Fedyukovich
- Arie Gurfinkel
- Lev Nachmanson
Author name cluster
Anna Becchi
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
2 papers
1 author row
Possible papers
2I&C Journal 2020 Journal Article
PPLite: Zero-overhead encoding of NNC polyhedra
- Anna Becchi
- Enea Zaffanella
We present an alternative Double Description representation for the domain of NNC (not necessarily closed) polyhedra, together with the corresponding Chernikova-like conversion procedure. The representation uses no slack variable at all and provides a solution to a few technical issues caused by the encoding of an NNC polyhedron as a closed polyhedron in a higher dimension space. We then reconstruct the abstract domain of NNC polyhedra, providing all the operators needed to interface it with commonly available static analysis tools: while doing this, we highlight the efficiency gains enabled by the new representation and we show how the canonicity of the new representation allows for the specification of proper, semantic widening operators. A thorough experimental evaluation shows that our new abstract domain achieves significant efficiency improvements with respect to classical implementations for NNC polyhedra.