Convex Invariant Refinement by Control Node Splitting: a Heuristic Approach

DOI10.1016/j.entcs.2012.10.007zbMath1294.68059OpenAlexW1978376998WikidataQ113318047 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

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

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

This page was built for publication: Convex Invariant Refinement by Control Node Splitting: a Heuristic Approach