PPLite: zero-overhead encoding of NNC polyhedra

DOI10.1016/J.IC.2020.104620MaRDI QIDQ2216124zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• A direct encoding for NNC polyhedra
• An efficient abstract domain for not necessarily closed polyhedra
• Not necessarily closed convex polyhedra and the double description method
• scientific article; zbMATH DE number 1948398
• Fast polyhedra abstract domain

Cites work

• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 1948398 (Why is no real title available?)
• scientific article; zbMATH DE number 2090855 (Why is no real title available?)
• scientific article; zbMATH DE number 3245483 (Why is no real title available?)
• scientific article; zbMATH DE number 3323651 (Why is no real title available?)
• scientific article; zbMATH DE number 3078984 (Why is no real title available?)
• A direct encoding for NNC polyhedra
• 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
• Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities
• An efficient abstract domain for not necessarily closed polyhedra
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• Automatic synthesis of switching controllers for linear hybrid systems: safety control
• Computing convex hulls and counting integer points with \texttt{polymake}
• Computing the face lattice of a polytope from its vertex-facet incidences
• Efficient constraint/generator removal from double description of polyhedra
• Fast polyhedra abstract domain
• Hybrid Systems: Computation and Control
• New modification of the double description method for constructing the skeleton of a polyhedral cone
• Not necessarily closed convex polyhedra and the double description method
• On the efficiency of convex polyhedra
• Precise widening operators for convex polyhedra
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Widening and narrowing operators for abstract interpretation

Cited in

(6)

• \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability
• Efficient convex zone merging in parametric timed automata
• Decoupling the ascending and descending phases in abstract interpretation
• Not necessarily closed convex polyhedra and the double description method
• A direct encoding for NNC polyhedra
• Symbolic analysis of linear hybrid automata -- 25 years later

Describes a project that uses

Uses Software

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

This page was built for publication: PPLite: zero-overhead encoding of NNC polyhedra

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2216124)