Applications of polyhedral computations to the analysis and verification of hardware and software systems

DOI10.1016/J.TCS.2009.07.033zbMATH Open1187.68311OpenAlexW2088667970MaRDI QIDQ1035700FDOQ1035700

Authors: Roberto Bagnara, Patricia M. Hill, Enea Zaffanella 

Publication date: 4 November 2009

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2009.07.033

Recommendations

• scientific article; zbMATH DE number 1948398
• Not necessarily closed convex polyhedra and the double description method
• Exact join detection for convex polyhedra and other numerical abstractions
• Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools
• scientific article; zbMATH DE number 2090855

zbMATH Keywords

abstract interpretationstatic analysiscomputer-aided verification

Mathematics Subject Classification ID

Reasoning under uncertainty in the context of artificial intelligence (68T37) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• HyTech: A model checker for hybrid systems
• Hybrid Systems: Computation and Control
• Title not available (Why is that?)
• SPHIN: a model checker for reconfigurable hybrid systems based on SPIN
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Affine relationships among variables of a program
• Precise widening operators for convex polyhedra
• Not necessarily closed convex polyhedra and the double description method
• Title not available (Why is that?)
• Title not available (Why is that?)
• A framework for numeric analysis of array operations
• Algorithm for discovering the set of all the solutions of a linear programming problem
• The algorithmic analysis of hybrid systems
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Title not available (Why is that?)
• Verification, Model Checking, and Abstract Interpretation
• Two variables per linear inequality as an abstract domain
• Grids: A Domain for Analyzing the Distribution of Numerical Values
• Title not available (Why is that?)
• Abstract Interpretation Frameworks
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• A unifying framework for several cutting plane methods for semidefinite programming
• Constraint propagation with interval labels
• How good are convex hull algorithms?
• Convexity recognition of the union of polyhedra
• Verifying generalized soundness of workflow nets
• Formal Modeling and Analysis of Timed Systems
• A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
• Grammar semantics, analysis and parsing by abstract interpretation
• Some ways to reduce the space dimension in polyhedra computations
• Title not available (Why is that?)
• On Fourier's algorithm for linear arithmetic constraints
• Tools and Algorithms for the Construction and Analysis of Systems
• Combinations of abstract domains for logic programming: Open product and generic pattern construction
• cTI: a constraint-based termination inference tool for ISO-Prolog
• Title not available (Why is that?)
• Static Analysis
• Static Analysis

Cited In (13)

• Efficient constraint/generator removal from double description of polyhedra
• A new look at the automatic synthesis of linear ranking functions
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• PPLite: zero-overhead encoding of NNC polyhedra
• Efficient elimination of redundancies in polyhedra by raytracing
• Accelerating Fourier-Motzkin elimination using bit pattern trees
• Static contract checking with abstract interpretation
• Title not available (Why is that?)
• Parametric verification and test coverage for hybrid automata using the inverse method
• Exact join detection for convex polyhedra and other numerical abstractions
• On finite linear systems containing strict inequalities
• Not necessarily closed convex polyhedra and the double description method
• Revisiting polyhedral analysis for hybrid systems

Uses Software

• SPIN
• PHAVer
• HyTech
• PPL
• PolyLib
• ASTREE
• SPHIN

This page was built for publication: Applications of polyhedral computations to the analysis and verification of hardware and software systems

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