Thanks to the work of Bruno Blanchet definite clauses are an established technique for verifying security properties of communication protocols. We investigate the expressive power of this approach with respect to verifying authenticity. A translation from protocols into definite clauses is given, and direct proofs for correctness and completeness of the authenticity verification based on these clauses are shown. These proofs are new, and in particular the completeness result is surprising. These results, beside their intrinsic value, shed light on some interesting issues about existing proposals for exploiting definite clauses in protocols verification.

Reduced product of abstract domains is a rather well-known operation for domain composition in abstract interpretation. In this article, we study its inverse operation, introducing a notion of domain complementation in abstract interpretation. Complementation provides as systematic way to design new abstract domains, and it allows to systematically decompose domains. Also, such an operation allows to simplify domain verification problems, and it yields space-saving representations for complex domains. We show that the complement exists in most coses, and we apply complementation to three well-know abstract domains, notably to Cousot and Cousot's interval domain for integer variable analysis, to Cousot and Cousot's domain for comportment analysis of functional languages, and to the domain Sharing for aliasing analysis of logic languages.

The abstract domain Prop for analyzing variable groundness in logic programs is considered. This domain consists of (equivalence classes of) propositional formulas whose propositional variables correspond to program variables with truth assignments indicating which program variables are ground. Some ambiguity remains about precisely which formula should be included in Prop so that all interesting sets of program execution states (substitutions) have a unique representation. This ambiguity is clarified by characterizing, both semantically and syntactically, the appropriate definition of Prop. The use of propositional formulas for representing properties of substitutions of a different type than groundness, such as freeness and independence of variables, is discussed.>

article Abstract interpretation of logic programs: an abstract domain for groundness, sharing, freeness and compoundness analysis Share on Authors: Agostino Cortesi Dept. of Mathematics, University of Padova, Via Belzoni 7, I-35131 Padova, Italy Dept. of Mathematics, University of Padova, Via Belzoni 7, I-35131 Padova, ItalyView Profile , Gilbert Filé Dept. of Mathematics, University of Padova, Via Belzoni 7, I-35131 Padova, Italy Dept. of Mathematics, University of Padova, Via Belzoni 7, I-35131 Padova, ItalyView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 26Issue 9Sept. 1991 pp 52–61https://doi.org/10.1145/115866.115872Published:01 May 1991 23citation291DownloadsMetricsTotal Citations23Total Downloads291Last 12 Months4Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Theoretical results are presented on multi-pass (both left-to-right and alternating), multi-sweep, and multi-visit attribute grammars. For each of these, a pure type and a simple type are distinguished: The pure attribute grammars are defined by nondeterministic attribute evaluators, and the simple ones by the corresponding (usual) deterministic evaluators. The time complexity of deciding membership in these classes of attribute grammars is studied. In general, this is harder for the pure classes than for the simple ones, for which it is either polynomial or NP-complete. The expressive power of the eight classes is compared by studying the translations they can compute. It is shown that sweeps are more powerful than passes, and visits are more powerful than sweeps.