SCSS 2014: Papers with AbstractsPapers 

Abstract. Satisfiability Modulo Theories, SMT, solvers are used in many applications. These applications benefit from the power of tuned and scalable theorem proving technologies for supported logics and specialized theory solvers. SMT solvers are primarily used to determine whether formulas are satisfiable. Furthermore, when formulas are satisfiable, many applications need models that assign values to free variables. Yet, in many cases arbitrary assignments are insufficient, and what is really needed is an <i>optimal</i> assignment with respect to objective functions. So far, users of Z3, an SMT solver from Microsoft Research, build custom loops to achieve objective values. This is no longer necessary with νZ (newZ, or maxZ), an extension within Z3 that lets users formulate objective functions directly with Z3. Under the hood there is a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations. Objective functions are combined as either Pareto fronts, lexicographically, or each objective is optimized independently.  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. 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, heapspace, 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. 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 75% of the needed proof dependencies among the first 100 predictions, which is a comparable performance of such initial experiments on other largetheory corpora.  Abstract. We present Probabilistic Doxastic Temporal (PDT) Logic for streams, a formalism to reason about probabilistic beliefs and their infinite temporal evolution in multiagent systems. Extending previous work on PDT Logic, this formalism builds on a Markov chain model to represent infinite streams of possible worlds. Within these streams, it enables the quantification of beliefs through probability intervals as well as the representation of temporal relations and epistemic actions. We show how agents can update their beliefs with respect to their observations, provide a model for infinite streams of possible worlds and show how we can map clippings of these streams to finite time windows. Based on these time windows, we introduce an adoption of the semantics of PDT Logic for finite time frames, and show how this provides a means to overcome the limitation of finite time domains.  Abstract. In this paper we first present three sorts of constraints (positive, negative and conditional ones) to specify that certain patterns must be satisfied in a XML document. These constraints are built on boolean XPath patterns. We define a specification as a set of clauses whose literals are constraints. Then, to reason about these specifications, we study some sound rules which permit to infer, subsume or simplify clauses. The main goal is to design a refutation procedure (based on these rules) to test if a given specification is satisfiable or not. We have formally proven the soundness of our procedure and we study the completeness and termination of the proposed method.  Abstract. Program behavior may depend on parameters, which are either configured before compilation time, or provided at runtime, e.g., by sensors or other input devices. Parametric program analysis explores how different parameter settings may affect the program behavior.
In order to infer invariants depending on parameters, we introduce parametric strategy iteration. This algorithm determines the precise least solution of systems of integer equations depending on surplus parameters. Conceptually, our algorithm performs ordinary strategy iteration on the given integer system for all possible parameter settings in parallel. This is made possible by means of region trees to represent the occurring piecewise affine functions. We indicate that each required operation on these trees is polynomialtime if only constantly many parameters are involved.
Parametric strategy iteration for systems of integer equations allows to construct parametric integer interval analysis as well as parametric analysis of differences of integer variables. It thus provides a general technique to realize precise parametric program analysis if numerical properties of integer variables are of concern. 

