A Reachability Predicate for Analyzing Low-Level Software

DOI10.1007/978-3-540-71209-1_4zbMath1186.68108OpenAlexW1606540187MaRDI QIDQ5758100

Shaunak Chatterjee, Zvonimir Rakamarić, Shuvendu K. Lahiri, Shaz Qadeer

Publication date: 3 September 2007

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71209-1_4

Mathematics Subject Classification ID

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

Related Items (6)

Verification of heap manipulating programs with ordered data by extended forest automata ⋮ Satisfiability Modulo Theories ⋮ Verifying Heap-Manipulating Programs in an SMT Framework ⋮ Generalizing the Template Polyhedral Domain ⋮ Verification of Equivalent-Results Methods ⋮ Region Analysis for Race Detection

Uses Software

• Zap
• ESC/Java
• TVLA

This page was built for publication: A Reachability Predicate for Analyzing Low-Level Software