Anders Hast: Existing but not Explicit - The User Perspective in Scrum Projects in Practice Location: ITC 2115, Time: 14:15
Abstract: GeoMemories is an online application for visualizing the geospatial changes of the Italian landscape. Recently an article was accepted for a journal, which shows the challenges of stitching millions of photos together. It also give examples of how the image archive, hosted by the Aerofototeca Nazionale in Rome together with other photo archives, can be used to monitor the long time change of the landscape. Some improvements regarding image stitching will also be explained.
Magnus Myreen , University of Cambridge: Machine code, formal verification and functional programming Location: 1145, Time: 10:30
All programs run in the form of machine code. Ultimately, all formal software verification ought to reach down to this concrete form of execution and prove theorems about the actual ARM, x86 or PowerPC machine instructions that pass through the processor.
This talk presents techniques and tools that aid both verification of existing machine code (e.g. as produced by gcc) and tools that synthesise correct-by-construction machine code from high-level specifications (functions in logic). All of these tools have been implemented and used within the HOL4 theorem prover.
For post hoc verification, I describe a proof-producing decompiler that, given concrete machine code, returns a...read more »
Marcus Holm: Scientific Computing on Hybrid Architectures Location: ITC 2446, Time: 14:00
Opponent: Dr. Xing Cai, Senior Research Scientist at Simula Research Laboratory and Professor at the University of Oslo
The discussion will be held in English.
Abstract: Modern computer architectures, with multicore CPUs and GPUs or other accelerators, make stronger demands than ever on writers of scientific code.
Normally, the most efficient program has to be written - using a substantial effort - by expert programmers for a certain application on a particular computer.
This thesis deals with several algorithmic and technical approaches towards effectively satisfying the demand for high performance parallel scientific applications on hybrid computer architectures without incurring such a high cost in expert programmer time.
Efficient programming is accomplished by writing performance-portable code where performance-critical functionality is provided either by an optimized library or by adaptively selecting which computational tasks that are executed on the CPU and the accelerator.
Ass. Prof. Sharmishtha Mitra, Department of Mathematics & Statistics, Indian Institute of Technology Kanpur, India: Analysis of Life Testing Models under different censoring and stress acceleration schemes Location: ITC 2344, Time: 14:15
Traditional life data analysis analyzes time-to-failure data (of a product, system or component) obtained under normal operating conditions to quantify the life characteristics of the objects. Accelerated life test (ALT) is a popular experimental strategy to obtain information on life distributions of highly reliable products. The main idea is to submit materials to higher than usual environmental conditions, or stress, to ensure early failure. Data obtained from such an experiment need to be extrapolated to estimate lifetime distribution under normal conditions.
A Step-Stress life test is a particular type of ALT. We observe the failure times of the products at a particular stress level, and then change the stress to a different level. Failure times in the new stress level are observed, and the stress level is changed again and so on. There are several stress loading schemes - constant stress, step-stress, ramp-stress, progressive stress, etc. Introduction of stresses ensures a reasonable number of failures and reduces the experimental time. The stress structure and the lifetime distribution have to be combined to get the comprehensive ALT model.
The analysis relies on life and stress data or time-to-failure data at a specific stress level. Data are either complete or censored. In this talk we discuss various aspects of the exact inference for the two-parameter Exponential distribution (a standard life-time distribution) under Type-II Hybrid Censoring (a popular censoring method) and Bayesian analysis of different Hybrid and Progressive Life Tests. This would be followed by exact and approximate inference procedures for a Simple Step-Stress model under Exponential distribution with location and scale parameters. We shall further consider the order restricted Bayesian inference for the Exponential Simple Step-Stress Model. Finally, Bayesian analysis of Simple Step-stress Model under Weibull lifetimes (another standard lifetime distribution) would be discussed in brief.
David Broman : Modelyze: Embedding DSLs for Modeling and Analyzing Cyber-Physical Systems Location: 1112, Time: 10:30
Cyber-physical systems combine computations, networks, and physical processes. Modeling and analysis of such systems are vital engineering techniques to mange complexity and enable rapid prototyping. In particular, complex cyber-physical systems are heterogenous, requiring various model of computations. A key challenge is to provide both expressive modeling capabilities and mechanisms for analyzing these heterogenous systems. This talk explores a solution to this challenge based on domain-specific embedded languages. We introduce a host language, named Modelyze, in which various domain-specific modeling languages may be embedded. The key features of ...read more »