A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
From MaRDI portal
Publication:3512505
DOI10.1007/978-3-540-70545-1_35zbMath1155.68366MaRDI 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
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Analysis of Executable Software Models, Type-based amortized resource analysis with integers and arrays, Discovering invariants via simple component analysis, Cost analysis of object-oriented bytecode programs, Linear Absolute Value Relation Analysis, Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
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