Abstract interpretation and application to logic programs

DOI10.1016/0743-1066(92)90030-7zbMath0776.68024OpenAlexW2081810835MaRDI QIDQ4012706

Radhia Cousot, Patrick Cousot

Publication date: 27 September 1992

Published in: The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0743-1066(92)90030-7

zbMATH Keywords

semantics-based program analysisoperational semanticsGalois connectioninvariance propertiestransition systemdataflow analysisabstract fixpoint equationabstract interpretation of programssemantics approximationvariant of SLD-resolution

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17) General topics in the theory of software (68N01)

Related Items (only showing first 100 items - show all)

Checked corecursive streams: expressivity and completeness ⋮ Transformation-Enabled Precondition Inference ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Adversarial logic ⋮ Decoupling the ascending and descending phases in abstract interpretation ⋮ Automatic verification of parameterized networks of processes ⋮ Abstraction for non-ground answer set programs ⋮ Pair-independence and freeness analysis through linear refinement. ⋮ A generic framework for heap and value analyses of object-oriented programming languages ⋮ Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting ⋮ Soundness Conditions for Big-Step Semantics ⋮ Sound Non-statistical Clustering of Static Analysis Alarms ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ The role of linearity in sharing analysis ⋮ Why does Astrée scale up? ⋮ Accelerating program analyses in Datalog by merging library facts ⋮ Thread-modular analysis of release-acquire concurrency ⋮ An abstract interpretation framework for optimizing dynamic modular logic languages ⋮ Optimality in goal-dependent analysis of Sharing ⋮ Expression-Based Aliasing for OO–languages ⋮ Trace-Based Coinductive Operational Semantics for While ⋮ Certified Static Analysis by Abstract Interpretation ⋮ The octagon abstract domain ⋮ Relational string abstract domains ⋮ Program verification with interacting analysis plugins ⋮ Deriving escape analysis by abstract interpretation ⋮ An iterative approach to precondition inference using constrained Horn clauses ⋮ Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types ⋮ Refining and compressing abstract domains ⋮ Descending chains and narrowing on template abstract domains ⋮ Speeding up inferences using relevance reasoning: a formalism and algorithms ⋮ The quotient of an abstract interpretation ⋮ Finding suitable variability abstractions for lifted analysis ⋮ A Novel Test Case Generation Method for Prolog Programs Based on Call Patterns Semantics ⋮ Non-terminating processes in the situation calculus ⋮ Abstract interpretation of temporal concurrent constraint programs ⋮ Tabling with Sound Answer Subsumption ⋮ A new framework for declarative programming ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ Using Abstract Interpretation to Correct Synchronization Faults ⋮ Finding Relevant Templates via the Principal Component Analysis ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Applying abstract acceleration to (co-)reachability analysis of reactive programs ⋮ Discovering invariants via simple component analysis ⋮ Unnamed Item ⋮ The powerset operator on abstract interpretations ⋮ Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis^† ⋮ Control-flow analysis of function calls and returns by abstract interpretation ⋮ Generalizing Inference Systems by Coaxioms ⋮ Unnamed Item ⋮ Loop Summarization Using Abstract Transformers ⋮ Magic-sets for localised analysis of Java bytecode ⋮ The two variable per inequality abstract domain ⋮ Least solutions of equations over N ⋮ The complexity of Tarski's fixed point theorem ⋮ Incremental Abstract Interpretation ⋮ Maximal incompleteness as obfuscation potency ⋮ Transforming floundering into success ⋮ Unnamed Item ⋮ A Novel Derivation Framework For Definite Logic Program ⋮ Probabilistic Semantics and Program Analysis ⋮ A polymorphic type dependency analysis for logic programs ⋮ Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically ⋮ Correct Answers for First Order Logic ⋮ Predicate abstraction in a program logic calculus ⋮ A Scalable Segmented Decision Tree Abstract Domain ⋮ Transforming semantics by abstract interpretation ⋮ Measuring the confinement of probabilistic systems ⋮ Static extensivity analysis for \(\lambda\)-definable functions over lattices ⋮ Abstract interpretation of mobile systems ⋮ Improving precision of type analysis using non-discriminative union ⋮ Abstract interpretation based verification of temporal properties for BioAmbients ⋮ Learning solution preferences in constraint problems ⋮ Static Contract Checking with Abstract Interpretation ⋮ A Forward-Backward Abstraction Refinement Algorithm ⋮ Omission-Based Abstraction for Answer Set Programs ⋮ Non-disjunctive Numerical Domain for Array Predicate Abstraction ⋮ Abstract interpretation and types for systems biology ⋮ Precondition Inference from Intermittent Assertions and Application to Contracts on Collections ⋮ Access Analysis-Based Tight Localization of Abstract Memories ⋮ Bi-inductive structural semantics ⋮ Relational Abstract Domain of Weighted Hexagons ⋮ Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs ⋮ A Note on the Inversion Join for Polyhedral Analysis ⋮ Constructive Galois Connections ⋮ Uniform closures: Order-theoretically reconstructing logic program semantics and abstract domain refinements ⋮ On the interaction between sharing and linearity ⋮ Similarity-based SLD resolution and its role for web knowledge discovery ⋮ The reduced relative power operation on abstract domains ⋮ Template polyhedra and bilinear optimization ⋮ Endomorphisms for Non-trivial Non-linear Loop Invariant Generation ⋮ On the verification of finite failure ⋮ Managing the granularity of constraint-based analyses by rule transformation. ⋮ An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations. ⋮ Models and emerging trends of concurrent constraint programming ⋮ Constructive design of a hierarchy of semantics of a transition system by abstract interpretation ⋮ Logical optimality of groundness analysis ⋮ Approximate reasoning by similarity-based SLD resolution. ⋮ Generating invariants for non-linear hybrid systems ⋮ Verifying time partitioning in the DEOS scheduling kernel

This page was built for publication: Abstract interpretation and application to logic programs