Leaping Loops in the Presence of Abstraction

DOI10.1007/978-3-540-73368-3_50zbMath1135.68465OpenAlexW1670210142MaRDI QIDQ5429340

Orna Kupferman, Mooly Sagiv, Thomas Ball

Publication date: 29 November 2007

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8184

Mathematics Subject Classification ID

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

Related Items

Abstract interpretation of microcontroller code: intervals meet congruences, Ranking function synthesis for bit-vector relations, Verification and falsification of programs with loops using predicate abstraction, Smaller Abstractions for ∀CTL* without Next