Dedicated to the memory of Sebastian Danicic. We present a theory for slicing imperative probabilistic programs containing random assignments and “observe” statements for conditioning. We represent such programs as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions. This allows direct adaptation of standard machinery such as data dependence, postdominators, relevant variables, and so on, to the probabilistic setting. We separate the specification of slicing from its implementation: (1) first, we develop syntactic conditions that a slice must satisfy (they involve the existence of another disjoint slice such that the variables of the two slices are probabilistically independent of each other); (2) next, we prove that any such slice is semantically correct; (3) finally, we give an algorithm to compute the least slice. To generate smaller slices, we may in addition take advantage of knowledge that certain loops will terminate (almost) always. Our results carry over to the slicing of structured imperative probabilistic programs, as handled in recent work by Hur et al. For such a program, we can define its slice, which has the same “normalized” semantics as the original program; the proof of this property is based on a result proving the adequacy of the semantics of pCFGs w.r.t. the standard semantics of structured imperative probabilistic programs.

A general constraint solver simplifies the implementation of program analyses because constraint generation can then be separated from constraint solving. In return, a general solver often needs to sacrifice performance for generality. We describe a strategy that given a set of constraints first performs off-line optimizations (performed before the execution of the solver) which enable a solver to find (potential) equivalences between analysis variables so as to reduce the problem space and thus improve performance. The idea is that different analyses use different subsets of constraints. As a result, a specific property may hold for the subsets and a specific optimization can be conducted on the constraints.

The notion of control dependence underlies many program analysis and transformation techniques. Despite being widely used, existing definitions and approaches to calculating control dependence are difficult to apply directly to modern program structures because these make substantial use of exception processing and increasingly support reactive systems designed to run indefinitely. This article revisits foundational issues surrounding control dependence, and develops definitions and algorithms for computing several variations of control dependence that can be directly applied to modern program structures. To provide a foundation for slicing reactive systems, the article proposes a notion of slicing correctness based on weak bisimulation, and proves that some of these new definitions of control dependence generate slices that conform to this notion of correctness. This new framework of control dependence definitions, with corresponding correctness results, is even able to support programs with irreducible control flow graphs. Finally, a variety of properties show that the new definitions conservatively extend classic definitions. These new definitions and algorithms form the basis of the Indus Java slicer, a publicly available program slicer that has been implemented for full Java.

This paper specifies, via a Hoare-like logic, an interprocedural and flow sensitive (but termination insensitive) information flow analysis for object-oriented programs. Pointer aliasing is ubiquitous in such programs, and can potentially leak confidential information. Thus the logic employs independence assertions to describe the noninterference property that formalizes confidentiality, and employs region assertions to describe possible aliasing. Programmer assertions, in the style of JML, are also allowed, thereby permitting a more fine-grained specification of information flow policy.The logic supports local reasoning about state in the style of separation logic. Small specifications are used; they mention only the variables and addresses relevant to a command. Specifications are combined using a frame rule. An algorithm for the computation of postconditions is described: under certain assumptions, there exists a strongest postcondition which the algorithm computes.

In this paper we develop a sound and complete type and behaviour inference algorithm for a fragment of CML (Standard ML with primitives for concurrency). Behaviours resemble terms of a process algebra and yield a concise representation of the communications taking place during execution; types are mostly as usual except that function ypes and ‘delayed communication types’ are labelled by behaviours expressing the communications that will take place if the function is applied or the delayed action is activated. The development of the present paper improves a previously published algorithm in achieving completeness as well as soundness; this is due to an alternative strategy for generalising over types and behaviours.

article Properties of unfolding-based meta-level systems Share on Author: Torben Amtoft Hansen Computer Science Department, Aarhus University, Ny Munkegade, building 540, DK-8000 Ârhus C, Denmark Computer Science Department, Aarhus University, Ny Munkegade, building 540, DK-8000 Ârhus C, DenmarkView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 26Issue 9Sept. 1991 pp 243–254https://doi.org/10.1145/115866.115892Online:01 May 1991Publication History 6citation186DownloadsMetricsTotal Citations6Total Downloads186Last 12 Months5Last 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