Events

Upcoming events

Inverse Rendering

Shida Beigpour
Joint Lecture Series
01 Feb 2017, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
Photographs as well as video frames are two-dimensional projections of three-dimensional real-world scenes. Photorealistic Computer Graphic Imagery (CGI) is usually generated by "rendering" a sophisticated three-dimensional model of a realistic scene on to a virtual camera sensor. Such process is not invertible due to the high amount of data loss. Still both physically captured photographs and synthesized photos (CGI) contain considerable amount of information about the characteristics of the scene itself. Even naïve human viewers are able to infer important information about the scene e.g. shape material illumination distance and actions solely from a single image. This is indeed much more difficult for computer systems. Inverse rendering is one of the hot-topics in computer vision in which the goal is to estimate and model the three-dimensional scene and its illumination automatically given only one or a sparse set of images from the scene. This is by nature a highly under-constraint problem which makes it very complex to solve. Yet the advancements in computation and imaging technologies (e.g. depth sensors and light-field cameras) open new horizons in this field. Inverse rendering makes many interesting applications possible including: creating novel views of the scene/objects re-lighting detecting and altering the object materials in the photographs and augmented reality.  This talk provides a brief overview of some of the state-of-the-art inverse rendering techniques and datasets with a strong focus on addressing the complexities of real-world scenarios.

Recent events

Time for Text Mining and Information Retrieval

Jannik Strötgen
Joint Lecture Series
11 Jan 2017, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
Temporal information is an important aspect in any information space and has important characteristics that make it highly eligible to be exploited in diverse text mining and information retrieval scenarios. For quite a long time only the metadata of text documents (e.g. publication dates) has been considered but with recent improvements in natural language processing (NLP) temporal expressions occurring in the content of documents (e.g. "January 2016" "next week") can be extracted and interpreted efficiently with high quality. This is particularly valuable as in many types of documents temporal expressions do not only occur frequently but also play a crucial role e.g. to anchor events in time.

In this talk after explaining the basics and challenges of the NLP task "temporal tagging" I present our approach to enrich documents with temporal information. Then I showcase several application scenarios in which we exploit automatically extracted temporal annotations for search and exploration tasks. These range from temporal information retrieval for news articles via Wikipedia-based event extraction up to the exploration of fictitious happenings in literary texts in the context of digital humanities research.

Proving Performance Properties of Higher-order Functions with Memoization

Ravi Madhavan
SWS Colloquium
20 Dec 2016, 11:30 am - 1:30 pm
Kaiserslautern building G26, room 112 / simultaneous videocast to Saarbrücken building E1 5, room 029
Static verification of performance properties of programs is an important problem that has attracted great deal of research. However most existing tools infer best-effort upper bounds and hope that they match users expectations. In this talk I will present a system for specifying and verifying bounds on resources such as the number of evaluation steps and heap-allocated objects for functional Scala programs that may rely on lazy evaluation and memoization. In our system users can specify the desired resource bound as a template with numerical holes in the contracts of functions e.g. as "steps <= ? * size(list) + ?" along with other functional properties necessary for establishing the bounds. The system automatically infers values for the holes that will make the templates hold for all executions of the functions. For example the property that a function converting a propositional formula f into negation-normal form (NNF) takes time linear in the size of f can be expressed in the post-condition of the function using the predicate "steps <= ? * size(f) + ?" where size is a user-defined function counting the number of nodes in the syntax tree of the formula. Using our tool we have verified asymptotically precise bounds of several algorithms and data structures that rely on complex sharing of higher-order functions and memoization. Our benchmarks include balanced search trees like red-black trees and AVL trees Okasaki?s constant-time queues deques lazy data structures based on numerical representations such as lazy binomial heaps cyclic streams and dynamic programming algorithms. Some of the benchmarks have posed serious challenges to automatic as well as manual reasoning. The system is a part of the Leon verifier and can be tried online at "http://leondev.epfl.ch" ("Resource bounds" section).

Proving Performance Properties of Higher-order Functions with Memoization

Ravi Madhavan
SWS Colloquium
20 Dec 2016, 11:30 am - 1:30 pm
Kaiserslautern building G26, room 112 / simultaneous videocast to Saarbrücken building E1 5, room 029
Static verification of performance properties of programs is an important problem that has attracted great deal of research. However most existing tools infer best-effort upper bounds and hope that they match users expectations. In this talk I will present a system for specifying and verifying bounds on resources such as the number of evaluation steps and heap-allocated objects for functional Scala programs that may rely on lazy evaluation and memoization. In our system users can specify the desired resource bound as a template with numerical holes in the contracts of functions e.g. as "steps <= ? * size(list) + ?"  along with other functional properties necessary for establishing the bounds. The system automatically infers values for the holes that will make the templates hold for all executions of the functions.  For example the property that a function converting a propositional formula f into negation-normal form (NNF)  takes time linear in the size of f can be expressed in the post-condition of the function using the predicate "steps <= ? * size(f) + ?"   where size is a user-defined function counting the number of nodes in the syntax tree of the formula. Using our tool we have verified asymptotically precise bounds of several algorithms and data structures that rely on complex sharing of higher-order functions and memoization. Our benchmarks include balanced search trees like red-black trees and AVL trees Okasaki?s constant-time queues deques lazy data structures based on numerical representations such as lazy binomial heaps cyclic streams and dynamic programming algorithms. Some of the benchmarks have posed serious challenges to automatic as well as manual reasoning. The system is a part of the Leon verifier and can be tried online at "http://leondev.epfl.ch" ("Resource bounds" section).

References:   (a) Symbolic Resource Bound Inference For Functional Programs. Ravichandhran Madhavan and Viktor Kuncak. Computer Aided Verification CAV 2014 (b) Contract-based Resource Verification for Higher-order Functions with Memoization. Ravichandhran Madhavan Sumith Kulal and Viktor Kuncak. To appear in POPL 2017

Archive