SMT-Based Array Invariant Generation

DOI10.1007/978-3-642-35873-9_12zbMath1426.68056OpenAlexW71055133MaRDI QIDQ2926644

Enric Rodríguez-Carbonell, Daniel Larraz, Albert Rubio

Publication date: 3 November 2014

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

Full work available at URL: https://doi.org/10.1007/978-3-642-35873-9_12

zbMATH Keywords

SMTprogram correctnessinvariant generation

Mathematics Subject Classification ID

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

Related Items

Lingva: Generating and Proving Program Properties Using Symbol Elimination ⋮ Analyzing Array Manipulating Programs by Program Transformation ⋮ Lemmaless induction in trace logic ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Speeding up the Constraint-Based Method in Difference Logic