Making abstract models complete

Completeness is a key feature of abstract interpretation. It corresponds to exactness of the abstraction of fix-points and relies upon the need of absence of false alarms in static program analysis. Making abstract interpretation complete is therefore a major problem in approximating the semantics of programming languages. In this paper, we consider the problem of making abstract interpretations complete by minimally modifying the predicate transformer, i.e. the semantics, of a program. We study the mathematical properties of complete functions on complete lattices and prove the existence of minimal transformations of monotone functions to achieve completeness. We then apply minimal complete transformers to prove the minimality of standard program transformations in security, such as static program monitoring.

Download Full-text

Theoretical Aspects of Semantics-Based Language Implementation

DAIMI Report Series ◽

10.7146/dpb.v19i329.6561 ◽

1990 ◽

Vol 19 (329) ◽

Author(s):

Flemming Nielson

Keyword(s):

Programming Languages ◽

Program Analysis ◽

Code Generation ◽

Program Transformation ◽

Abstract Interpretation ◽

Language Implementation

The research summarised here concerns theoretical aspects involved in the implementation of programming languages directly from a description of their semantics. This involves a study of the subtasks abstract interpretation (a framework for program analysis), code generation and program transformation and the main aim has been to ensure the correctness of these subtasks.

Download Full-text

Semantic Foundations of Data Flow Analysis

DAIMI Report Series ◽

10.7146/dpb.v10i131.7585 ◽

1981 ◽

Vol 10 (131) ◽

Cited By ~ 1

Author(s):

Flemming Nielson

Keyword(s):

Program Analysis ◽

Abstract Interpretation ◽

Data Flow ◽

Flow Analysis ◽

Denotational Semantics ◽

System Of Equations ◽

Program Transformations ◽

Sensitive Data ◽

Data Flow Analysis ◽

Made In

Abstract Interpretation (P. Cousot, R. Cousot and others) is a method for program analysis that is able to describe many data flow analyses. We investigate and weaken the assumptions made in abstract interpretation and express abstract interpretation within Denotational Semantics. As an example we specify constant propagation.Some authors have used abstract interpretation to formulate ''available expressions'' (a so-called ''history-sensitive'' data flow analysis). Our development of ''available expressions'' is better justified, semantically.In traditional data flow analysis and abstract interpretation it is generally assumed that the ''Meet Over all Paths'' solution is wanted. We prove that the solution specified by our approach is the ''Meet Over all Paths'' solution to a certain system of equations obtained from the program.To indicate the usefulness of our approach we show how to validate a class of program transformations, including ''constant folding''.Throughout this paper we use a toy language consisting of declarations, expressions and commands (involving conditional and iteration). Excluded are procedures and jumps.

Download Full-text

Particpants' Proceedings on the Workshop: Types for Program Analysis

DAIMI Report Series ◽

10.7146/dpb.v24i493.7021 ◽

1995 ◽

Vol 24 (493) ◽

Author(s):

Hanne Riis Nielson ◽

Kirsten Lackner Solberg

Keyword(s):

Programming Languages ◽

Program Analysis ◽

Abstract Interpretation ◽

Recent Trend ◽

Type Systems ◽

Program Committee ◽

Program Optimization ◽

Proof Techniques ◽

Areas Of Interest

As a satellite meeting of the TAPSOFT'95 conference we organized a small workshop on program analysis. The title of the workshop, ``Types for Program Analysis´´, was motivated by the recent trend of letting the presentation and development of program analyses be influenced by annotated type systems, effect systems, and more general logical systems. The contents of the workshop was intended to be somewhat broader; consequently the call for participation listed the following areas of interest:- specification of specific analyses for programming languages,- the role of effects, polymorphism, conjunction/disjunction types, dependent types etc.in specification of analyses,- algorithmic tools and methods for solving general classes of type-based analyses,- the role of unification, semi-unification etc. in implementations of analyses,- proof techniques for establishing the safety of analyses,- relationship to other approaches to program analysis, including abstract interpretation and constraint-based methods,- exploitation of analysis results in program optimization and implementation.The submissions were not formally refereed; however each submission was read by several members of the program committee and received detailed comments and suggestions for improvement. We expect that several of the papers, in slightly revised forms, will show up at future conferences. The workshop took place at Aarhus University on May 26 and May 27 and lasted two half days.

Download Full-text

Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis

Proceedings of the ACM on Programming Languages ◽

10.1145/3498721 ◽

2022 ◽

Vol 6 (POPL) ◽

pp. 1-31

Author(s):

Marco Campion ◽

Mila Dalla Preda ◽

Roberto Giacobazzi

Keyword(s):

Program Analysis ◽

Program Verification ◽

Abstract Interpretation ◽

False Alarms ◽

Analysis Tool ◽

Number Of False Alarms ◽

Bounded Number ◽

Abstract Domains ◽

Metric Distance ◽

Made In

Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In abstract interpretation this corresponds to the release of false alarms, e.g., when it is used for program analysis and program verification. As all alarming systems, a program analysis tool is credible when few false alarms are reported. As a consequence, we have to live together with false alarms, but also we need methods to control them. As for all approximation methods, also for abstract interpretation we need to estimate the accumulated imprecision during program analysis. In this paper we introduce a theory for estimating the error propagation in abstract interpretation, and hence in program analysis. We enrich abstract domains with a weakening of a metric distance. This enriched structure keeps coherence between the standard partial order relating approximated objects by their relative precision and the effective error made in this approximation. An abstract interpretation is precise when it is complete. We introduce the notion of partial completeness as a weakening of precision. In partial completeness the abstract interpreter may produce a bounded number of false alarms. We prove the key recursive properties of the class of programs for which an abstract interpreter is partially complete with a given bound of imprecision. Then, we introduce a proof system for estimating an upper bound of the error accumulated by the abstract interpreter during program analysis. Our framework is general enough to be instantiated to most known metrics for abstract domains.

Download Full-text

Enriched Meanings

10.1093/oso/9780198847854.001.0001 ◽

2020 ◽

Author(s):

Ash Asudeh ◽

Gianluca Giorgolo

Keyword(s):

Cognitive Science ◽

Programming Languages ◽

Category Theory ◽

Worst Case ◽

Disciplinary Boundaries ◽

Semantics Of Programming Languages ◽

Basic Meaning ◽

Language Interpretation ◽

Major Branch ◽

Compositional Properties

This book presents a theory of enriched meanings for natural language interpretation. Certain expressions that exhibit complex effects at the semantics/pragmatics boundary live in an enriched meaning space while others live in a more basic meaning space. These basic meanings are mapped to enriched meanings just when required compositionally, which avoids generalizing meanings to the worst case. The theory is captured formally using monads, a concept from category theory. Monads are also prominent in functional programming and have been successfully used in the semantics of programming languages to characterize certain classes of computation. They are used here to model certain challenging linguistic computations at the semantics/pragmatics boundary. Part I presents some background on the semantics/pragmatics boundary, informally presents the theory of enriched meanings, reviews the linguistic phenomena of interest, and provides the necessary background on category theory and monads. Part II provides novel compositional analyses of the following phenomena: conventional implicature, substitution puzzles, and conjunction fallacies. Part III explores the prospects of combining monads, with particular reference to these three cases. The authors show that the compositional properties of monads model linguistic intuitions about these cases particularly well. The book is an interdisciplinary contribution to Cognitive Science: These phenomena cross not just the boundary between semantics and pragmatics, but also disciplinary boundaries between Linguistics, Philosophy and Psychology, three of the major branches of Cognitive Science, and are here analyzed with techniques that are prominent in Computer Science, a fourth major branch. A number of exercises are provided to aid understanding, as well as a set of computational tools (available at the book's website), which also allow readers to develop their own analyses of enriched meanings.

Download Full-text

Completions of ordered magmas

Fundamenta Informaticae ◽

10.3233/fi-1980-3109 ◽

1980 ◽

Vol 3 (1) ◽

pp. 105-116

Author(s):

Bruno Courcelle ◽

Jean-Claude Raoult

Keyword(s):

Programming Languages ◽

Semantics Of Programming Languages ◽

Ordered Algebras ◽

Completion Theorem

We give a completion theorem for ordered magmas (i.e. ordered algebras with monotone operations) in a general form. Particular instances of this theorem are already known, and new results follow. The semantics of programming languages is the motivation of such investigations.

Download Full-text