PPLite: zero-overhead encoding of NNC polyhedra

DOI10.1016/j.ic.2020.104620zbMath1496.68351OpenAlexW3047969355MaRDI QIDQ2216124

Anna Becchi, Enea Zaffanella

Publication date: 15 December 2020

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2020.104620

zbMATH Keywords

static analysisconvex polyhedradouble descriptionstrict inequalities

Mathematics Subject Classification ID

Computational aspects related to convexity (52B55) Computer graphics; computational geometry (digital and algorithmic aspects) (68U05)

Related Items

\textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability ⋮ Symbolic analysis of linear hybrid automata -- 25 years later ⋮ Decoupling the ascending and descending phases in abstract interpretation ⋮ Efficient convex zone merging in parametric timed automata

Uses Software

• Apron
• polymake
• PHAVer
• HyTech
• 4ti2
• PPL
• PAGAI
• polco
• efmtool

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficient constraint/generator removal from double description of polyhedra
• Automatic synthesis of switching controllers for linear hybrid systems: safety control
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• Computing the face lattice of a polytope from its vertex-facet incidences
• On the efficiency of convex polyhedra
• Widening and narrowing operators for abstract interpretation
• Computing convex hulls and counting integer points with \texttt{polymake}
• Precise widening operators for convex polyhedra
• Not necessarily closed convex polyhedra and the double description method
• New modification of the double description method for constructing the skeleton of a polyhedral cone
• Hybrid Systems: Computation and Control
• Fast polyhedra abstract domain
• Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities
• Algorithm for discovering the set of all the solutions of a linear programming problem
• Algorithm for finding a general formula for the non-negative solutions of a system of linear equations
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• An efficient abstract domain for not necessarily closed polyhedra
• A direct encoding for NNC polyhedra