Systematic design of program transformation frameworks by abstract interpretation

DOI10.1145/503272.503290zbMath1323.68356OpenAlexW2008609084MaRDI QIDQ5178905

Patrick Cousot, Radhia Cousot

Publication date: 17 March 2015

Published in: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/503272.503290

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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

Pair-independence and freeness analysis through linear refinement. ⋮ Extending separation logic with fixpoints and postponed substitution ⋮ Abstract Program Slicing ⋮ Abstract interpretation as automated deduction ⋮ Structural Invariants for the Verification of Systems with Parameterized Architectures ⋮ Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data ⋮ Automatic Inference of Access Permissions ⋮ Ideal Abstractions for Well-Structured Transition Systems ⋮ Lattice-based refinement in bounded model checking ⋮ The map equality domain ⋮ Toward Compact Abstractions for Processor Pipelines ⋮ Hardware Trojan detection via rewriting logic ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Abstract Interpretation as Automated Deduction ⋮ Enhancing the implementation of mathematical formulas for fixed-point and floating-point arithmetics ⋮ Combining Model Reductions ⋮ An empirical study on classification methods for alarms from a bug-finding static C analyzer ⋮ Probabilistic Analysis of Programs: A Weak Limit Approach ⋮ An Introduction to Certificate Translation ⋮ Certified Static Analysis by Abstract Interpretation ⋮ Relational string abstract domains ⋮ Fast three-valued abstract bit-vector arithmetic ⋮ Software watermarking: a semantics-based approach ⋮ Characterization and computation of ancestors in reaction systems ⋮ Refining and compressing abstract domains ⋮ Descending chains and narrowing on template abstract domains ⋮ Semantics of Probabilistic Programs: A Weak Limit Approach ⋮ Analyzing the environment structure of higher-order languages using frame strings ⋮ Inferring complete initialization of arrays ⋮ Finding suitable variability abstractions for lifted analysis ⋮ Inference of Field-Sensitive Reachability and Cyclicity ⋮ Logical Characterizations of Behavioral Relations on Transition Systems of Probability Distributions ⋮ On invariant checking ⋮ Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case ⋮ A Systematic Approach to Probabilistic Pointer Analysis ⋮ Mathematical programming: Turing completeness and applications to software analysis ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ Stabilizing Floating-Point Programs Using Provenance Analysis ⋮ Conjunctive Abstract Interpretation Using Paramodulation ⋮ Transforming Abstract Interpretations by Abstract Interpretation ⋮ Hiding Software Watermarks in Loop Structures ⋮ Splitting the Control Flow with Boolean Flags ⋮ Semantics-based software watermarking by abstract interpretation ⋮ Gradual type-and-effect systems ⋮ Abstract interpretation of database query languages ⋮ Generalizing the Paige-Tarjan algorithm by abstract interpretation ⋮ Abstract allocation as a unified approach to polyvariance in control-flow analyses ⋮ Loop Summarization Using Abstract Transformers ⋮ Context-sensitive analysis without calling-context ⋮ An abstract interpretation-based model for safety semantics ⋮ A survey of strategies in rule-based program transformation systems ⋮ Linear Absolute Value Relation Analysis ⋮ Abstract Diagnosis of First Order Functional Logic Programs ⋮ Optimality and condensing of information flow through linear refinement ⋮ Approximating Probabilistic Behaviors of Biological Systems Using Abstract Interpretation ⋮ Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation ⋮ Maximal incompleteness as obfuscation potency ⋮ The abstract domain of trapezoid step functions ⋮ Building Certified Static Analysers by Modular Construction of Well-founded Lattices ⋮ Probabilistic Semantics and Program Analysis ⋮ Accurate Evaluation of Arithmetic Expressions (Invited Talk) ⋮ Generic Abstraction of Dictionaries and Arrays ⋮ Operational Semantics for Reexecution-based Analysis of Logic Programs with Delay Declarations ⋮ On the Relations between Disjunctive and Linear Logic Programming ⋮ Refining and Compressing Abstract Model Checking1 1The work is partially supported by MURST project: Certificazione automatica di programmi mediante interpretazione astratta. ⋮ Logic programs as specifications in the inductive verification of logic programs ⋮ A Scalable Segmented Decision Tree Abstract Domain ⋮ Using abstract interpretation to add type checking for interfaces in Java bytecode verification ⋮ Abstract interpretation based verification of temporal properties for BioAmbients ⋮ Abstracting Nash equilibria of supermodular games ⋮ Abstract Certification of Global Non-interference in Rewriting Logic ⋮ Static Contract Checking with Abstract Interpretation ⋮ Comparison of abstract interpretations ⋮ Precondition Inference from Intermittent Assertions and Application to Contracts on Collections ⋮ Strengthening Induction-Based Race Checking with Lightweight Static Analysis ⋮ String Analysis as an Abstract Interpretation ⋮ Information Leakage Analysis by Abstract Interpretation ⋮ Transformation of a PID controller for numerical accuracy ⋮ Weakening additivity in adjoining closures ⋮ Bi-inductive structural semantics ⋮ View-Augmented Abstractions ⋮ Relational Abstract Domain of Weighted Hexagons ⋮ A Spectrum of Behavioral Relations over LTSs on Probability Distributions ⋮ A relational shape abstract domain ⋮ Abstract Interpretation from a Topological Perspective ⋮ Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships ⋮ Sound and Complete Abstract Graph Transformation ⋮ A new abstraction framework for affine transformers ⋮ Model Checking Erlang Programs – Abstracting Recursive Function Calls ⋮ An efficient simulation algorithm based on abstract interpretation ⋮ On the verification of finite failure ⋮ Parsing as abstract interpretation of grammar semantics ⋮ An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations. ⋮ A theory of observables for logic programs ⋮ Semantic Abstraction and Quantum Computation ⋮ On Probabilistic Techniques for Data Flow Analysis ⋮ Logical optimality of groundness analysis ⋮ Analysis of the equality relations for the program terms ⋮ Abstract cofibered domains: Application to the alias analysis of untyped programs ⋮ Regular algebra applied to language problems

Uses Software

• CVT

This page was built for publication: Systematic design of program transformation frameworks by abstract interpretation