Search

Diese Dissertation untersucht sowohl den methodischen als auch den empirischen Aspekt einiger Bayesscher nichtparametrischer Methoden, die auf univariate und multivariate zeitvariable finanzielle Volatilitätsmodelle angewendet werden. Die damit verbundenen Probleme bestehen nicht nur in dem Entwerfen einer geeigneten Modellstruktur, die die gewünschte Modellierungsflexibilität sicherstellt, sondern auch in dem Gestalten eines effizienten Sampling-Algorithmus. Der Dirichlet Process Mixture (DPM)-basierte Ansatz ermöglicht flexible In-Sample-Schätzungen und liefert Dichteprognosen für univariate und hochdimensionale Probleme. Der flexible Rahmen kann auf viele hochdimensionale Aspekte der Finanzmarktmodellierung angewendet werden, wie beispielsweise auf die Analyse von der gemeinsamen Bewegung von Volatilitäten, sowie von Strukturen der Volatilitätsübertragung. This thesis explores both the methodological and the empirical aspect of certain Bayesian nonparametric methods applied to time-varying financial volatility modeling in the univariate and the multivariate cases. The related issues involve not only designing an appropriate model structure, which provides the desired modeling flexibility, but also accordingly constructing an efficient sampling algorithm. The DPM-based approach allows flexible in-sample estimation and also provides density forecasts for univariate and high-dimensional problems. The flexible framework can be applied to many high-dimensional financial market modeling aspects, such as analyzing volatility co-movements and patterns of volatility transmission.

Modular verification of the functional behaviour of a concurrent program remains a challenge. We propose a new way to achieve this, using histories, modelled as process algebra terms, to keep track of local changes. When threads terminate or synchronise in some other way, local histories are combined into global histories, and by resolving the global histories, the reachable state properties can be determined. Our logic is an extension of permission-based separation logic, which supports expressive and intuitive specifications. We discuss soundness of the approach, and illustrate it on several examples.

This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.

SECTION 1 ROBUST AND MULTIVARIATE DATA ANALYSIS

SECTION 1 ROBUST AND MULTIVARIATE DATA ANALYSIS

Conference of 2016 Multimedia Benchmark Workshop, MediaEval 2016 ; Conference Date: 20 October 2016 Through 21 October 2016; Conference Code:125011; International audience; This paper provides an overview of the Retrieving Diverse Social Images task that is organized as part of the Media-Eval 2016 Benchmarking Initiative for Multimedia Evaluation. The task addresses the problem of result diversification in the context of social photo retrieval where images, metadata, text information, user tagging profiles and content and text models are available for processing. We present the task challenges, the proposed data set and ground truth, the required participant runs and the evaluation metrics.

Run-time assertion checking of multithreaded programs is challenging, as assertion evaluation should not interfere with the execution of other threads. This paper describes the prototype implementation of a run-time assertion checker that achieves this by evaluating assertions over snapshots of the state, instead of over the live state. Our prototype e-OpenJML, an extension to OpenJML, provides an easy to use, safe and interference-free evaluation of JML specifications in multithreaded programs. To achieve this, it integrates e-STROBE, our extension to the STROBE framework for asynchronous assertion evaluation. e-STROBE prevents all possible interferences between assertion evaluation and other program threads, which the original STROBE can not. It also simplifies evaluating assertions that relate the value of expressions in multiple states.

Modular verification of the functional behaviour of a concurrent program remains a challenge. We propose a new way to achieve this, using histories, modelled as process algebra terms, to keep track of local changes. When threads terminate or synchronise in some other way, local histories are combined into global histories, and by resolving the global histories, the reachable state properties can be determined. Our logic is an extension of permission-based separation logic, which supports expressive and intuitive specifications. We discuss soundness of the approach, and illustrate it on several examples.

Specifying the functional behaviour of a concurrent program can often be quite troublesome: it is hard to provide a stable method contract that can not be invalidated by other threads. In this paper we propose a novel modular technique for specifying and verifying behavioural properties in concurrent programs. Our approach uses history-based specifications. A history is a process algebra term built of actions, where each action represents an update over a heap location. Instead of describing the object's precise state, a method contract may describe the method's behaviour in terms of actions recorded in the history. The client class can later use the history to reason about the concrete state of the object. Our approach allows providing simple and intuitive specifications, while the logic is a simple extension of permission-based separation logic.

Class invariants are a highly useful feature for the verification of object-oriented programs, because they can be used to capture all valid object states. In a sequential program setting, the validity of class invariants is typically described in terms of a visible state semantics, i.e., invariants only have to hold whenever a method begins or ends execution, and they may be broken inside a method body. However, in a concurrent setting, this restriction is no longer usable, because due to thread interleavings, any program state is potentially a visible state. In this paper we present a new approach for reasoning about class invariants in multithreaded programs. We allow a thread to explicitly break an invariant at specific program locations, while ensuring that no other thread can observe the broken invariant. We develop our technique in a permission-based separation logic environment. However, we deviate from separation logic's standard rules and allow a class invariant to express properties over shared memory locations (the invariant footprint), independently of the permissions on these locations. In this way, a thread may break or reestablish an invariant without holding permissions to all locations in its footprint. To enable modular verification, we adopt the restrictions of Muller's ownership-based type system.

This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based specifications: instead of describing method behaviour in terms of the object's state, we specify it in terms of the object's state history. A history is defined as a list of state updates, which at all points can be related to the actual object's state. We illustrate the approach on the BlockingQueue hierarchy from the java.util.concurrent library. We show how the behaviour of the interface BlockingQueue is specified, leaving a few decisions open to descendant classes. The classes implementing the interface correctly inherit the specifications. As a specification language, we use a combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures., Comment: In Proceedings FLACOS 2012, arXiv:1209.1699

DOI: 10.1023/A:1012085714353; International audience

102 ref.; International audience

National audience