ABSTRACT. A meaning formula for a symbolic algorithm is a statement that captures the mathematical relationship between the input and output expressions of the algorithm. We examine how meaning formulas can be expressed and proved in a formal logic and how they can be used to represent mathematical knowledge and to define mathematical services.

ABSTRACT. We report the results of the first experiments with learning proof dependencies from the formalizations done with the Coq system. We explain the process of obtaining the dependencies from the Coq proofs, the characterization of formulas that is used for the learning, and the evaluation method. Various machine learning methods are compared on a dataset of 5021 toplevel Coq proofs coming from the CoRN repository. The best resulting method covers on average 73% of the needed proof dependencies among the first 100 predictions, which is a comparable performance of such initial experiments on other large-theory corpora.

ABSTRACT. JavaScript programs have access to a wide range of resources and many of those have security implications. Tight bounds on the consumption of those resources can give indication of the functionality provided by the program and minimize the security risks of mobile applications. Resource consumption is typically dependent on the input of the user. In this paper we introduce an amortized type system for a core of JavaScript. The resulting types certify bounds for the resource usage dependent on the input parameters. We define the amortized types and the corresponding typing rules. Furthermore we discuss how to fully automatically infer those resource bounds for arbitrary applications. In addition to the usual example of amortized resource, heap-space, our type system can be applied to many phone specific resources, which we demonstrate using the example of the GPS sensor and others. The main result of this paper is the soundness of the core type system, proving that a valid type for a program corresponds to a bound on the units used of the specified resource.

ABSTRACT. One of the issues with traditional mutation testing is the possible large number of mutants generated. In this work, we illustrate how the concept of relative correctness can guide the generation and selection of mutants when repairing a loop program. We show that fewer and better mutants can be generated , thus adding efficiency by reducing the huge computational cost associated with mutation analysis.

ABSTRACT. Termination is the property of a program to complete its execution after a finite number of operations. Abort freedom is the property of a program to complete its execution without attempting an illegal operation, such as a division by zero, an arithmetic overflow, an array reference out of bounds, a reference to a nil pointer, etc. We present an approach to the analysis of iterative programs in which these two aspects are merged into a single formula. We illustrate our approach on a number of examples, and we compare our findings to related work on termination and on abort freedom.