SCSS 2014: Papers with Abstracts

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 (new-Z, or max-Z), 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, 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. 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 large-theory corpora.

Abstract. We present Probabilistic Doxastic Temporal (PDT) Logic for streams, a formalism to reason about
probabilistic beliefs and their infinite temporal evolution in multi-agent 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 polynomial-time 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.