Elimination Techniques for Program Analysis

DOI10.1007/978-3-642-37651-1_8MaRDI QIDQ4916078zbMATH OpenOpenAlexFDO

Authors 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

Quantifier elimination, model completeness, and related topics (03C10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Reduction and quantifier elimination techniques for program validation
• Program analysis using quantifier-elimination heuristics (extended abstract)
• Iterative-free program analysis
• scientific article; zbMATH DE number 1324833
• Eliminating proofs from programs
• Elimination of loop invariants in program verification
• Program Extraction in Constructive Analysis
• scientific article; zbMATH DE number 2018591

Cites work

• A Practical Decision Procedure for Arithmetic with Function Symbols
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Automatic Generation of Polynomial Loop Invariants
• Basic principles of mechanical theorem proving in elementary geometries
• Computer Aided Verification
• Constraint-based verification of parameterized cache coherence protocols
• Generating all polynomial invariants in simple loops
• scientific article; zbMATH DE number 44444 (Why is no real title available?)
• scientific article; zbMATH DE number 48269 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1234104 (Why is no real title available?)
• scientific article; zbMATH DE number 3303655 (Why is no real title available?)
• Interprocedurally Analyzing Polynomial Identities
• Non-linear loop invariant generation using Gröbner bases
• Precise interprocedural analysis through linear algebra
• Programming Languages and Systems
• Static Analysis
• Static Analysis
• The derivation of systolic computations
• The synthesis of loop predicates

Cited in

(3)

• Lingva: generating and proving program properties using symbol elimination
• On strongest algebraic program invariants
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs

This page was built for publication: Elimination Techniques for Program Analysis

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