A Reachability Predicate for Analyzing Low-Level Software

DOI10.1007/978-3-540-71209-1_4MaRDI QIDQ5758100zbMATH OpenOpenAlexFDO

Authors Shaunak Chatterjee, Shuvendu K. Lahiri, Zvonimir Rakamarić, 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

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

Recommendations

• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• Verification, Model Checking, and Abstract Interpretation
• Predicate abstraction for linked data structures
• Verification, Model Checking, and Abstract Interpretation
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

Cited in

(11)

• Reachability-based acyclicity analysis by abstract interpretation
• Generalizing the template polyhedral domain
• Verification of heap manipulating programs with ordered data by extended forest automata
• Satisfiability modulo theories
• Region Analysis for Race Detection
• Verifying Heap-Manipulating Programs in an SMT Framework
• Theoretical Computer Science
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• Verification of Equivalent-Results Methods
• Low-level reachability analysis based on formal logic
• Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)

Describes a project that uses

Uses Software

• Zap
• ESC/Java
• TVLA

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5758100)