Principles of abstract interpretation

MaRDI QIDQ5857678zbMATH OpenFDO

Authors Patrick Cousot

Publication date 2 April 2021

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) General topics in the theory of software (68N01) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstract interpretation
• scientific article; zbMATH DE number 2087617
• scientific article; zbMATH DE number 1324833
• Abstract interpretation from a denotational-semantics perspective
• scientific article; zbMATH DE number 1200752

Cited in

(27)

• Intensional Kleene and Rice theorems for abstract program semantics
• Structural-Abstraction Principles
• Abstract interpretation
• scientific article; zbMATH DE number 2087617 (Why is no real title available?)
• Sweeping in Abstract Interpretation
• String abstract domains and their combination
• Asynchronous correspondences between hybrid trajectory semantics
• Limits and difficulties in the design of under-approximation abstract domains
• Lifting numeric relational domains to algebraic data types
• Deciding program properties via complete abstractions on bounded domains
• Exploiting Modularity of SOS Semantics to Define Quantitative Extensions of Reaction Systems
• Logics for extensional, locally complete analysis via domain refinements
• Abstract interpretation of recursive logic definitions for efficient runtime assertion checking
• Exploiting adjoints in property directed reachability analysis
• Broadening the applicability of local completeness analysis with intensional and extensional guarantees
• Separability and non-determinizability of WSTS
• An input-output relational domain for algebraic data types and functional arrays
• Memory-efficient fixpoint computation
• Cone-based abstract interpretation for nonlinear positive invariant synthesis
• A correctness and incorrectness program logic
• Canonical forms and widening for two variables per inequality systems
• On the design of program logics
• Regular model checking for systems with effectively regular reachability relation
• Model checking as program verification by abstract interpretation
• Adjointness in property directed reachability analysis
• Abstract Lipschitz continuity. Combining semantic and quantitative approximations
• Refining abstract interpretations

This page was built for publication: Principles of abstract interpretation

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