Loop invariant synthesis in a combined abstract domain

DOI10.1016/j.jsc.2012.08.007zbMath1256.68044OpenAlexW2146373156MaRDI QIDQ1930180

Shengchao Qin, Xin Chen, Chenguang Luo, Guanhua He, Wei-Ngan Chin

Publication date: 10 January 2013

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2012.08.007

zbMATH Keywords

abstractionnumerical analysisshape analysisseparation logicloop invariantcombining analysisfixpoint analysis

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Verification of heap manipulating programs with ordered data by extended forest automata ⋮ Counterexample Validation and Interpolation-Based Refinement for Forest Automata ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification

Uses Software

• Dafny

This page was built for publication: Loop invariant synthesis in a combined abstract domain