Recursive assertions and parallel programs

Summary We prove that recursive assertions are enough for proofs of parallel programs considered in Owicki and Gries [7]. In other words, we prove that for any parallel program S and recursive assertions p and q if {p} S{q} is true under the standard interpretation in natural numbers then all intermediate assertions needed in the proof can be chosen recursive. Finally, we show that if auxiliary variables are used only as program counters then the above result does not hold.     

Nondeterministic flowchart programs with recursive procedures: semantics and correctness I

In this paper, we study some aspects of the semantics of nondeterministic flowchart programs with recursive procedures. In the first part of this work we provide the operational semantics of programs using the concept of an execution tree. We propose a new definition of the semantics of a non-deterministic recursive program as a mapping from the input domain to the set of execution trees determined by the program. Using this new concept, we prove that every nondeterministic flowchart program with recursive procedures can be unfolded into a semantically equivalent infinite pure flowchart (without procedures). This result is applied in the second part of this work to prove the soundness of an inductive assertion method which is also complete with a finite number of assertions (contrary to De Bakker and Meertens's method [11]).     

PROPER:一个概率程序终止性与正确性分析工具

概率程序将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面,它有助于定性和定量地分析仿射概率程序的终止性,可以验证该概率程序是否以概率1终止,估计期望终止时间的上限,并计算步数N,使得N步后给定程序的终止概率呈指数下降;另一方面,它可以估计一个断言成立的概率区间,这有助于分析变量不确定性对概率程序结果的影响.通过实验表明,PROPER对分析各种仿射概率程序是有效的.     

Detecting races in Relay Ladder Logic programs

Relay Ladder Logic (RLL) [5] is a programming language widely used for complex embedded control applications such as manufacturing and amusement park rides. The cost of bugs in RLL programs is extremely high, often measured in millions of dollars (for shutting down a factory) or human safety (for rides). In this paper, we describe our experience in applying constraint-based program analysis techniques to analyze production RLL programs. Our approach is an interesting combination of probabilistic testing and program analysis, and we show that our system is able to detect bugs with high probability, up to the approximations made by the conservative program analysis. We demonstrate that our analysis is useful in detecting some flaws in production RLL programs that are difficult to find by other techniques.     

Compiler Analysis of the Value Ranges for Variables

Programs can be analyzed to determine bounds on the ranges of values assumed by variables at various points in the program. This range information can then be used to eliminate redundant tests, verify correct operation, choose data representations, select code to be generated, and provide diagnostic information. Sophisticated analyses involving the proofs of complex assertions are sometimes required to derive accurate range information for the purpose of proving programs correct. The performance of such algorithms may be unacceptable for the routine analysis required during the compilation process. This paper presents a discussion of mechanical range analysis employing techniques practical for use in a compiler. This analysis can also serve as a useful adjunct to the more sophisticated techniques required for program proving.     

Reflexive transitive invariant relations: A basis for computing loop functions

Invariant assertions play an important role in the analysis and verification of iterative programs. In this paper, we introduce a related but distinct concept, namely that of invariant relation. While invariant assertions are useful to prove the correctness of a loop with respect to a specification (represented by a precondition/ postcondition pair) in Hoare’s logic, invariant relations are useful to derive the function of the loop in Mills’ logic.     

Demonic, angelic and unbounded probabilistic choices in sequential programs

Probabilistic predicate transformers extend standard predicate transformers by adding probabilistic choice to (transformers for) sequential programs; demonic nondeterminism is retained. For finite state spaces, the basic theory is set out elsewhere [17], together with a presentation of the probabilistic ‘healthiness conditions’ that generalise the ‘positive conjunctivity’ of ordinary predicate transformers. Here we expand the earlier results beyond ordinary conjunctive transformers, investigating the structure of the transformer space more generally: as Back and von Wright [1] did for the standard (non-probabilistic) case, we nest deterministic, demonic and demonic/angelic transformers, showing how each subspace can be constructed from the one before. We show also that the results hold for infinite state spaces. In the end we thus find characteristic healthiness conditions for the hierarchies of a system in which deterministic, demonic, probabilistic and angelic choices all coexist. Received: 10 November 1998 / 7 September 2000     

Some applications of topology to program semantics

The relationship between programs and the set of partial correctness assertions that they satisfy, constitutes a Galois connection. The topology resulting from this Galois connection is closely related to the Lindenbaum baum topology for the language in which these partial correctness assertions are stated. This relationship provides us with a tool for understanding the incompleteness of Hoare Logics and for answering certain natural questions about the connection between the relational semantics and the partial correctness assertion semantics for programs, especially in connection with the question of modularity of programs. Two questions to which we shall find topological answers in this paper are “When is a language expressive for a program?”, and “When can we have rules of inference which are adequate to infer the properties of the complex program ±#β from those of its components ±,β?” We also obtain a natural answer to the question “What can the set{(A, B)|{A}±{B} is true) look like for arbitraryα?”.     

A Note on Synthesis of Inductive Assertions

One of the principal impediments to widespread use of automated program verification methodology is due to the user burden of creating appropriate inductive assertions. In this paper, we investigate a class of programs for which such inductive assertions can be mechanically generated from Input-output specifications. This class of programs, called accumulating programs, are iterative realizations of problems in which the required output information is accumulated during successive passes over the input data structures. Obtaining invariant assertions for such programs is shown to be equivalent to the problem of generalizations of specifications to that over an extended closed data domain. For this purpose, a set of basis data elements are to be conceived of as generating the extended domain. An arbitary data element would thus be considered as uniquely decomposable into a sequence of basis elements. The structural relations between the components of a data element are used to extend program behavior and thus obtain the desired invariant.     

The software model checker Blast

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to Blast and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use Blast to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use Blast to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, Blast determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that Blast can provide automated, precise, and scalable analysis for C programs.     

Content reference: Reasoning about rules

In a companion paper [1] we described the concept of saturation, the situation in a program in which so many knowledge sources (KSs) are potentially useful at each invocation cycle that it is unrealistic to consider unguided, exhaustive invocation. We argued that saturation appears almost inevitable in large AI programs.We suggested that the process of invocation can be viewed as occurring in three steps: retrieval (selecting some subset of KSs from the knowledge base), refinement (pruning or reordering that subset), and execution (executing one or more of the KSs). We then argued that one useful approach to dealing with saturation is by embedding intelligence in the refinement phase, and described meta-rules, a means of encoding knowledge used to effect refinement.In this paper we consider a more detailed, ‘engineering’ issue, but one with a number of interesting implications: While there are many ways to implement refinement, we suggest that one particular technique—which we call content reference—offers a number of advantages, including giving the system some ability to reason about the content of its knowledge.     

Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings

By following a rely-guarantee style of reasoning, we present novel termination and cost analyses for concurrent programs that, in order to prove termination or infer the cost of a considered loop: (1) infer the termination/cost of each loop as if it were a sequential one, imposing assertions on how shared-data is modified concurrently; and then (2) prove that these assertions cannot be violated infinitely many times and, for cost analysis, infer how many times they are violated. At the core of the analysis, we use a may-happen-in-parallel analysis to restrict the set of program points whose execution can interleave. Interestingly, the same kind of reasoning can be applied to prove termination and infer upper bounds on the number of iterations of loops with concurrent interleavings. To the best of our knowledge, this is the first method to automatically bound the cost of such kind of loops. We have implemented our analysis for an actor-based language, and showed its accuracy and efficiency by applying it on several typical applications for concurrent programs and on an industrial case study.     

Causal independence for probability assessment and inference usingBayesian networks

A Bayesian network is a probabilistic representation for uncertain relationships, which has proven to be useful for modeling real-world problems. When there are many potential causes of a given effect, however, both probability assessment and inference using a Bayesian network can be difficult. In this paper, we describe causal independence, a collection of conditional independence assertions and functional relationships that are often appropriate to apply to the representation of the uncertain interactions between causes and effect. We show how the use of causal independence in a Bayesian network can greatly simplify probability assessment as well as probabilistic inference     

Automating exception-safety classification

Exception handling mechanisms provide a structured way to deal with exceptional circumstances, making it easier to read and reason about programs. Exception handling, however, cannot avoid the problem that the transfer of control might leave the program in an inconsistent state—resources might leak, invariants might be violated, the program state might be changed. Since client code often needs to know how a program behaves in the presence of exceptions, the exception-safety classification distinguishes three different classes of safety guarantees; this classification is used, for example, during the review process in the Boost organization for standardized libraries in C++. Classifying the safety level of a procedure requires understanding program invariants and tracking program state at any given point in the code, which is error-prone when done by hand. Yet, no tool support is available to date. In this paper we present the first automated analysis for exception guarantees. Since the safety level of an arbitrary procedure is undecidable, the analysis conservatively approximates exception safety . The analysis is based on the theory of backward data-flow analysis and recognizes two of the three safety guarantees, the strong and the no-throw guarantee, and provides counterexamples otherwise. A prototype implementation is available.     

Refinement algebra for probabilistic programs

We identify a refinement algebra for reasoning about probabilistic program transformations in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled or terminates respectively. As well as developing the basic theory of the algebra we demonstrate how it may be used to explain key differences and similarities between standard (i.e. non-probabilistic) and probabilistic programs and verify important transformation theorems for probabilistic action systems.     

On Probabilistic Techniques for Data Flow Analysis

We present a semantics-based technique for analysing probabilistic properties of imperative programs. This consists in a probabilistic version of classical data flow analysis. We apply this technique to pWhile programs, i.e programs written in a probabilistic version of a simple While language. As a first step we introduce a syntax based definition of a linear operator semantics (LOS) which is equivalent to the standard structural operational semantics of While. The LOS of a pWhile program can be seen as the generator of a Discrete Time Markov Chain and plays a similar role as a collecting or trace semantics for classical While. Probabilistic Abstract Interpretation techniques are then employed in order to define data flow analyses for properties like Parity and Live Variables.     

A logic-based approach to program flow analysis

A formalism is presented for tracking assertions which hold universally, i.e., at the end of all the execution paths to a given program point, and assertions which hold existentially, i.e., at the end of some execution paths. In the formalism, the assertions which hold at a given execution path are uniformly defined by an entry environment which contains the assertions which hold when the execution of the program begins and an environment transformer for every program construct. The novel aspect of our formalism is that Horn clauses are used to specify the consistent environments and the meaning of program constructs. The best iterative algorithm (a notion defined by P. Cousot and R. Cousot) for tracking universal and existential assertions simultaneously is given. Conditions are presented under which the best iterative algorithm can be efficiently implemented. The formalism is applied to the pointer equality problem in Pascal. It is shown that universal pointer equalities may be used to reduce the number of superfluous existential equalities, and that existential equalities may be used to obtain more universal equalities. Recent empirical results indicate that tracking the combination of may and must equalities leads to substantial improvements in the result of the analysis. For programs without recursively defined records, the best iterative algorithm can be effectively implemented. These results apply to multiple levels of pointers and can be extended to handle possibly recursive procedures. However, for programs with recursively defined data types further approximations are necessary, e.g., by using a finite graph to model all the possible pointer equalities. For simplicity, this paper does not present an analysis algorithm for this case. Received: 2 September 1991 / 25 June 1997     

LATTICEEASY: A program for lattice simulations of scalar fields in an expanding universe

We describe a C++ program that we have written and made available for calculating the evolution of interacting scalar fields in an expanding universe. The program is particularly useful for the study of reheating and thermalization after inflation. The program and its full documentation are available on the Web at http://www.science.smith.edu/departments/Physics/fstaff/gfelder/latticeeasy/. In this paper we provide a brief overview of what the program does and what it is useful for.

Program summary

Program title: LATTICEEASYCatalog identifier: AEAW_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/AEAW_v1_0.htmlProgram obtainable from: CPC Program Library, Queen's University, Belfast, N. IrelandLicensing provisions: Standard CPC licence, http://cpc.cs.qub.ac.uk/licence/licence.htmlNo. of lines in distributed program, including test data, etc.: 2579No. of bytes in distributed program, including test data, etc.: 34 521Distribution format: tar.gzProgramming language: C++Computer: AnyOperating system: AnyRAM: Typically 4 MB to 800 MBClassification: 1.9Nature of problem: After inflation the universe consisted of interacting fields in a high energy, nonthermal state [1]. The evolution of these fields can not be described with standard approximation techniques such as linearization, kinetic theory, or Hartree expansion, and must thus be simulated numerically. Fortunately, the fields rapidly acquire large occupation numbers over a range of frequencies, so their evolution can be accurately modeled with classical field theory [2]. The specific fields and interactions relevant at these high energies are not known, so different models must be tested phenomenologically.Solution method: LATTICEEASY solves the equations of motion for interacting scalar fields in an expanding universe. The user describes a particular theory by entering the field potential and its derivatives in a “model file” and the program then uses a staggered leapfrog method to evolve the field equations and Friedmann equation for the fields and the expansion of the universe.Restrictions: In its current form LATTICEEASY only includes scalar fields and does not include metric perturbations.Running time: The running time can range from minutes to weeks.References: [1] A.D. Linde, Particle Physics and Inflationary Cosmology, Harwood, Chur, Switzerland, 1990. [2] S. Khlebnikov, I. Tkachev, Phys. Rev. Lett. 77 (1996) 219, hep-ph 9603378.     

Writing friendly programs in modular form

Friendly software is defined as computer programs which can be run interactively and profitably without incurring fatal errors causing execution termination. We discuss a modular library and a simple program structure providing for input validation, help, status, overview and change commands in a standard FORTRAN environment. As an illustration we show how program WONPSE [Computers Chem.13, 201 (1989)] was easily transformed from a conventional program into a friendly tool for frontier research and student training on N-electron symmetry-eigenfunctions.