Possibly not closed convex polyhedra and the Parma Polyhedra Library. The domain of convex polyhedra is employed in several systems for the analysis and verification of hardware and software components. Current applications span imperative, functional and logic languages, synchronous languages and synchronization protocols, real-time and hybrid systems. Since the seminal work of P. Cousot and N. Halbwachs, convex polyhedra have thus played an important role in the formal methods community and several critical tasks rely on their software implementations. Despite this, existing libraries for the manipulation of convex polyhedra are still research prototypes and suffer from limitations that make their usage problematic, especially in critical applications. Furthermore, there is inadequate support for polyhedra that are Not Necessarily Closed (NNC), i.e., polyhedra that are described by systems of constraints where strict inequalities are allowed to occur. This paper presents the Parma Polyhedra Library, a new, robust and complete implementation of NNC convex polyhedra, concentrating on the distinctive features of the library and on the novel theoretical underpinnings. (Source: http://freecode.com/)

References in zbMATH (referenced in 97 articles , 1 standard article )

Showing results 1 to 20 of 97.
Sorted by year (citations)

1 2 3 4 5 next

  1. Becchi, Anna; Zaffanella, Enea: PPLite: zero-overhead encoding of NNC polyhedra (2020)
  2. Ben-Amram, Amir M.; Hamilton, Geoff: Tight polynomial worst-case bounds for loop programs (2020)
  3. Fajardo, María D.; Goberna, Miguel A.; Rodríguez, Margarita M. L.; Vicente-Pérez, José: Even convexity and optimization. Handling strict inequalities (2020)
  4. García Soto, Miriam; Prabhakar, Pavithra: Abstraction based verification of stability of polyhedral switched systems (2020)
  5. Perry, John: A dynamic F4 algorithm to compute Gröbner bases (2020)
  6. Yang, Jung-Min; Moor, Thomas; Raisch, Jörg: Refinements of behavioural abstractions for the supervisory control of hybrid systems (2020)
  7. Doménech, Jesús J.; Gallagher, John P.; Genaim, Samir: Control-flow refinement by partial evaluation, and its application to termination and cost analysis (2019)
  8. Gronski, Jessica; Ben Sassi, Mohamed-Amin; Becker, Stephen; Sankaranarayanan, Sriram: Template polyhedra and bilinear optimization (2019)
  9. Hampe, Simon; Joswig, Michael; Schröter, Benjamin: Algorithms for tight spans and tropical linear spaces (2019)
  10. Zolotykh, Nikolai Yu.; Bastrakov, Sergei I.: Two variations of graph test in double description method (2019)
  11. Avis, David; Jordan, Charles: \textttmplrs: a scalable parallel vertex/facet enumeration code (2018)
  12. Bezděk, Peter; Beneš, Nikola; Černá, Ivana; Barnat, Jiří: On clock-aware LTL parameter synthesis of timed automata (2018)
  13. Boutonnet, Rémy; Halbwachs, Nicolas: Improving the results of program analysis by abstract interpretation beyond the decreasing sequence (2018)
  14. De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio: Solving Horn clauses on inductive data types without induction (2018)
  15. Doyen, Laurent; Frehse, Goran; Pappas, George J.; Platzer, André: Verification of hybrid systems (2018)
  16. Jovanović, Aleksandra; Kwiatkowska, Marta: Parameter synthesis for probabilistic timed automata using stochastic game abstractions (2018)
  17. Kafle, Bishoksan; Gallagher, John P.; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: An iterative approach to precondition inference using constrained Horn clauses (2018)
  18. Kafle, Bishoksan; Gallagher, John P.; Ganty, Pierre: Tree dimension in verification of constrained Horn clauses (2018)
  19. Majumdar, Rupak; Raskin, Jean-François: Symbolic model checking in non-Boolean domains (2018)
  20. Payet, Étienne; Spoto, Fausto: Checking array bounds by abstract interpretation and symbolic expressions (2018)

1 2 3 4 5 next

Further publications can be found at: http://bugseng.com/products/ppl/documentation/bibliography