Abstract interpretation and application to logic programs

DOI10.1016/0743-1066(92)90030-7MaRDI QIDQ4012706zbMATH OpenOpenAlexFDO

Authors Patrick Cousot, Radhia 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

Galois connectionoperational semanticstransition systeminvariance propertiesdataflow analysissemantics-based program analysisabstract fixpoint equationabstract interpretation of programssemantics approximationvariant of SLD-resolution

Mathematics Subject Classification ID

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

Recommendations

• Publication:3201751
• Bottom-up abstract interpretation of logic programs
• Abstract interpretation of resolution-based semantics
• scientific article; zbMATH DE number 512885
• A practical framework for theabstract interpretation of logic programs

Cited in

(only showing first 100 items - show all)

• Finding suitable variability abstractions for lifted analysis
• The two variable per inequality abstract domain
• Abstract interpretation and types for systems biology
• Making abstract domains condensing
• scientific article; zbMATH DE number 879006 (Why is no real title available?)
• Models and emerging trends of concurrent constraint programming
• Abstract interpretation based on Alexander Templates
• scientific article; zbMATH DE number 1696888 (Why is no real title available?)
• The octagon abstract domain
• Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis^†
• Trace-Based Coinductive Operational Semantics for While
• Abstract interpretation of logic programs using magic transformations
• An abstract interpretation framework for optimizing dynamic modular logic languages
• A freeness and sharing analysis of logic programs based on a pre-interpretation
• An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations.
• Pair-independence and freeness analysis through linear refinement.
• Magic-sets for localised analysis of Java bytecode
• The role of linearity in sharing analysis
• Precondition inference from intermittent assertions and application to contracts on collections
• Why does Astrée scale up?
• Interpreting abstract interpretations in membership equational logic
• Non-terminating processes in the situation calculus
• Design of abstract domains using first-order logic
• Automatic verification of parameterized networks of processes
• Extending abstract acceleration methods to data-flow programs with numerical inputs
• Relational abstract domain of weighted hexagons
• Maximal incompleteness as obfuscation potency
• The complexity of Tarski's fixed point theorem
• Similarity-based SLD resolution and its role for web knowledge discovery
• Predicate Abstraction in a Program Logic Calculus
• Incremental Abstract Interpretation
• A novel derivation framework for definite logic program
• Abstract interpretation of resolution-based semantics
• Abstract interpretation of temporal concurrent constraint programs
• Abstract interpretation based on oldt resolution
• Symbolic model checking in non-Boolean domains
• Certified Static Analysis by Abstract Interpretation
• A practical framework for theabstract interpretation of logic programs
• Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting
• Learning solution preferences in constraint problems
• scientific article; zbMATH DE number 7037626 (Why is no real title available?)
• Reduced models for efficient CCS verification
• Verifying time partitioning in the DEOS scheduling kernel
• Finite-tree analysis for constraint logic-based languages
• Bottom-up abstract interpretation of logic programs
• scientific article; zbMATH DE number 3978439 (Why is no real title available?)
• Precise goal-independent abstract interpretation of constraint logic programs
• Analyzing logic programs using “prop”-ositional logic programs and a magic wand
• Program Development in Computational Logic
• Internal and External Logics of Abstract Interpretations
• Propositional Interpolation and Abstract Interpretation
• Optimality in goal-dependent analysis of Sharing
• On the verification of finite failure
• Access analysis-based tight localization of abstract memories
• scientific article; zbMATH DE number 1954120 (Why is no real title available?)
• Managing the granularity of constraint-based analyses by rule transformation.
• On the interaction between sharing and linearity
• The quotient of an abstract interpretation
• Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
• scientific article; zbMATH DE number 1942465 (Why is no real title available?)
• Uniform closures: Order-theoretically reconstructing logic program semantics and abstract domain refinements
• Efficient bottom-up execution of logic programs using abstract interpretation
• Sound non-statistical clustering of static analysis alarms
• Bi-inductive structural semantics
• A new framework for declarative programming
• Logic Programming
• Improving precision of type analysis using non-discriminative union
• Optimized algorithms for incremental analysis of logic programs
• Soundness conditions for big-step semantics
• Precise goal-independent abstract interpretation of constraint logic programs.
• Constructive Galois connections
• Combinations of abstract domains for logic programming: Open product and generic pattern construction
• Resource usage analysis of logic programs via abstract interpretation using sized types
• Loop Summarization Using Abstract Transformers
• Immediate fixpoints and their use in groundness analysis
• Specialisation of Prolog and FCP programs using abstract interpretation
• Expression-Based Aliasing for OO–languages
• Transforming floundering into success
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• A mode analysis of logic programs by abstract interpretation
• Sequence-based abstract interpretation of Prolog
• A generic framework for heap and value analyses of object-oriented programming languages
• Predicate abstraction in a program logic calculus
• Approximate reasoning by similarity-based SLD resolution.
• Abstraction for non-ground answer set programs
• Deriving escape analysis by abstract interpretation
• Bottom-up dataflow analysis of normal logic programs
• Using abstract interpretation to correct synchronization faults
• Measuring the confinement of probabilistic systems
• Transforming semantics by abstract interpretation
• Least solutions of equations over N
• Refining and compressing abstract domains
• scientific article; zbMATH DE number 549957 (Why is no real title available?)
• scientific article; zbMATH DE number 7453192 (Why is no real title available?)
• A Forward-Backward Abstraction Refinement Algorithm
• Path dependent analysis of logic programs
• Applying abstract acceleration to (co-)reachability analysis of reactive programs
• Discovering invariants via simple component analysis
• scientific article; zbMATH DE number 4178750 (Why is no real title available?)
• Correct answers for first order logic

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

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