Lifting abstract interpreters to quantified logical domains
From MaRDI portal
Publication:3189843
DOI10.1145/1328438.1328468zbMath1295.68085OpenAlexW2132251441MaRDI QIDQ3189843
Sumit Gulwani, Bill McCloskey, Ashish Kumar Tiwari
Publication date: 12 September 2014
Published in: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1328438.1328468
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (17)
Verifying Array Manipulating Programs with Full-Program Induction ⋮ Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Synthesis of positive logic programs for checking a class of definitions with infinite quantification ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Convergence: integrating termination and abort-freedom ⋮ The Undefined Domain: Precise Relational Information for Entities That Do Not Exist ⋮ Analyzing Array Manipulating Programs by Program Transformation ⋮ Completeness and expressiveness of pointer program verification by separation logic ⋮ Abstract interpretation of microcontroller code: intervals meet congruences ⋮ An array content static analysis based on non-contiguous partitions ⋮ An Assume Guarantee Approach for Checking Quantified Array Assertions ⋮ Static Contract Checking with Abstract Interpretation ⋮ Symbolic String Verification: Combining String Analysis and Size Analysis ⋮ Non-disjunctive Numerical Domain for Array Predicate Abstraction ⋮ Abstraction Refinement for Quantified Array Assertions ⋮ Algorithmic Analysis of Array-Accessing Programs
This page was built for publication: Lifting abstract interpreters to quantified logical domains
