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

DOI10.1016/j.tcs.2009.07.033zbMath1187.68311OpenAlexW2088667970MaRDI QIDQ1035700

Roberto Bagnara, Enea Zaffanella, Patricia M. Hill

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

zbMATH Keywords

static analysisabstract interpretationcomputer-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)

Related Items

Efficient constraint/generator removal from double description of polyhedra, On finite linear systems containing strict inequalities, Efficient Elimination of Redundancies in Polyhedra by Raytracing, PPLite: zero-overhead encoding of NNC polyhedra, Exact join detection for convex polyhedra and other numerical abstractions, A new look at the automatic synthesis of linear ranking functions, Static Contract Checking with Abstract Interpretation, Applications of polyhedral computations to the analysis and verification of hardware and software systems, PARAMETRIC VERIFICATION AND TEST COVERAGE FOR HYBRID AUTOMATA USING THE INVERSE METHOD, Accelerating Fourier–Motzkin elimination using bit pattern trees

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Grammar semantics, analysis and parsing by abstract interpretation
• The algorithmic analysis of hybrid systems
• On Fourier's algorithm for linear arithmetic constraints
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Some ways to reduce the space dimension in polyhedra computations
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• Constraint propagation with interval labels
• Affine relationships among variables of a program
• How good are convex hull algorithms?
• A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
• Combinations of abstract domains for logic programming: Open product and generic pattern construction
• HyTech: A model checker for hybrid systems
• Precise widening operators for convex polyhedra
• Not necessarily closed convex polyhedra and the double description method
• Two Variables per Linear Inequality as an Abstract Domain
• A unifying framework for several cutting plane methods for semidefinite programming
• Verifying Generalized Soundness of Workflow Nets
• Grids: A Domain for Analyzing the Distribution of Numerical Values
• cTI: a constraint-based termination inference tool for ISO-Prolog
• A framework for numeric analysis of array operations
• Abstract Interpretation Frameworks
• Static Analysis
• Algorithm for discovering the set of all the solutions of a linear programming problem
• Hybrid Systems: Computation and Control
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Static Analysis
• Formal Modeling and Analysis of Timed Systems
• Verification, Model Checking, and Abstract Interpretation
• Tools and Algorithms for the Construction and Analysis of Systems
• Convexity recognition of the union of polyhedra