Convex Invariant Refinement by Control Node Splitting: a Heuristic Approach

DOI10.1016/j.entcs.2012.10.007zbMath1294.68059WikidataQ113318047 ScholiaQ113318047MaRDI QIDQ5170180

Vivien Maisonneuve

Publication date: 22 July 2014

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2012.10.007

zbMATH Keywords

transformermodel checkingprogram analysisautomatic invariant detectionCFG restructuring

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q42: Grammars and rewriting systems

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Computing invariants with transformers: experimental scalability and accuracy

Uses Software

• Aspic
• SPEED

Cites Work

• A Modular Static Analysis Approach to Affine Loop Invariants Detection
• Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs
• Convex Partitions of Polyhedra: A Lower Bound and Worst-Case Optimal Algorithm
• Combining Widening and Acceleration in Linear Relation Analysis
• SPEED: Symbolic Complexity Bound Analysis
• Computing the Transitive Closure of a Union of Affine Integer Tuple Relations
• A new solution of Dijkstra's concurrent programming problem
• Lazy abstraction
• SPEED
• Programming Languages and Systems