Iterating Octagons

DOI10.1007/978-3-642-00768-2_29MaRDI QIDQ3617767zbMATH OpenOpenAlexFDO

Authors Marius Bozga, Codruţa Gîrlea, Radu Iosif

Publication date 31 March 2009

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-00768-2_29

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Automata and formal grammars in connection with logical questions (03D05) First-order arithmetic and fragments (03F30) Formal languages and automata (68Q45)

Recommendations

• PTIME computation of transitive closures of octagonal relations
• Incrementally closing octagons
• Automated Technology for Verification and Analysis
• Flat Parametric Counter Automata
• Safety problems are NP-complete for flat integer programs with octagonal loops

Cites work

• A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages
• A Logic of Singly Indexed Arrays
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• Automated Technology for Verification and Analysis
• Flat Parametric Counter Automata
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• Iterating Octagons
• On iterating linear transformations over recognizable sets of integers
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• The octagon abstract domain
• What Else Is Decidable about Integer Arrays?

Cited in

(19)

• CTL* model checking for data-aware dynamic systems with arithmetic
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Computing linear arithmetic representation of reachability relation of one-counter automata
• PTIME computation of transitive closures of octagonal relations
• Incrementally closing octagons
• Using basis dependence distance vectors in the modified Floyd-Warshall algorithm
• Verification of gap-order constraint abstractions of counter systems
• Using basis dependence distance vectors to calculate the transitive closure of dependence relations by means of the Floyd-Warshall algorithm
• Verification of gap-order constraint abstractions of counter systems
• Safety problems are NP-complete for flat integer programs with octagonal loops
• Interprocedural reachability for flat integer programs
• A new acceleration-based combination framework for array properties
• Fast acceleration of ultimately periodic relations
• Iterating Octagons
• Bounded underapproximations
• A calculus for modular loop acceleration
• Access-based localization for octagons
• Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
• Algebraic program analysis

Describes a project that uses

Uses Software

• FLATA

This page was built for publication: Iterating Octagons

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