PPLite: zero-overhead encoding of NNC polyhedra

DOI10.1016/J.IC.2020.104620zbMATH Open1496.68351OpenAlexW3047969355MaRDI QIDQ2216124FDOQ2216124

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

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

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)

Cites Work

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

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

Uses Software

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

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)