Elimination Techniques for Program Analysis

DOI10.1007/978-3-642-37651-1_8zbMath1383.68023MaRDI QIDQ4916078

Deepak Kapur

Publication date: 19 April 2013

Published in: Programming Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-37651-1_8

Mathematics Subject Classification ID

68Q55: Semantics in the theory of computing

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

03C10: Quantifier elimination, model completeness, and related topics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• The derivation of systolic computations
• Basic principles of mechanical theorem proving in elementary geometries
• Constraint-based verification of parameterized cache coherence protocols
• Generating all polynomial invariants in simple loops
• Non-linear loop invariant generation using Gröbner bases
• Precise interprocedural analysis through linear algebra
• A Practical Decision Procedure for Arithmetic with Function Symbols
• Automatic Generation of Polynomial Loop Invariants
• The synthesis of loop predicates
• Interprocedurally Analyzing Polynomial Identities
• Static Analysis
• Static Analysis
• Programming Languages and Systems
• Computer Aided Verification