A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis

DOI10.1007/978-3-540-70545-1_35zbMath1155.68366OpenAlexW1492171827MaRDI QIDQ3512505

Bhargav S. Gulavani, Sumit Gulwani

Publication date: 15 July 2008

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

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

Mathematics Subject Classification ID

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

Related Items (6)

Discovering invariants via simple component analysis ⋮ Type-based amortized resource analysis with integers and arrays ⋮ Linear Absolute Value Relation Analysis ⋮ Analysis of Executable Software Models ⋮ Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships ⋮ Cost analysis of object-oriented bytecode programs

Cites Work

• Unnamed Item
• Unnamed Item
• Non-linear loop invariant generation using Gröbner bases
• Precise interprocedural analysis through linear algebra
• Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems
• Array Abstractions from Proofs
• Ranking Abstractions
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Automata, Languages and Programming
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis