On August 27, 2018

Speaker

Ilya Sergey (UCL / 조교수)


Title

Fast Synthesis of Programs that Alter Data Structures


Abstract

In my talk, I will describe a deductive approach for synthesizing imperative programs with pointers from declarative specifications expressed in Separation Logic. The approach treats logical program specifications, given in the form or pre- and postconditions with a pure and a spatial part, as proof goals, and provides an algorithm for rule-directed program construction based on the shape of the symbolic heap footprint a desired program manipulates.

The program synthesis algorithm rests on the novel framework of Synthetic Separation Logic (SSL), which generalises the classical notion of heap entailment P |- Q from Separation Logic to incorporate a possibility of transforming a heap satisfying an assertion P so the result would satisfy an assertion Q. A synthesized program represents a proof term for a transforming entailment statement P ~> Q, and the synthesis procedure corresponds to a proof search. The produced executable programs are, thus, correct by construction, in the sense that they satisfy the ascribed pre/postconditions, and are accompanied by complete proof derivations (i.e., certificates), which can be checked independently by a third-party verifier.

The approach has been implemented as a proof search engine for SSL in a form the program synthesizer called SuSLik. For efficiency, the engine exploits properties of SSL specifications, aggressively relying on a version of the Frame Rule and commutativity of separating conjunction to prune the search space. I will explain and showcase the use of SSL on characteristic examples, describe the design of SuSLik, and report on the experience of using it to synthesize a series of benchmark programs manipulating with heap-based linked data structures.


Bio

Prof Ilya Sergey does research in the area of programming languages (PL), program analysis and formal verification. In recent years, He has mainly been concerned with developing scalable methods for building trustworthy concurrent and distributed software with application to consensus protocols and blockchains, but his earlier work was advancing the state of the art in static analysis for higher-order languages and PL design.

Prior to joining academia, Ilya has spent a part of his career in industry, working in JetBrains Inc., a world-leading company in creating integrated development environments for software developers. He obtained his PhD at KU Leuven (Belgium), and was a postdoctoral researcher at IMDEA Software Institute (Spain) and a Lecturer (Assistant Professor) at University College London (UK). He will be taking an appointment as a tenure-track Assistant Professor at Yale-NUS College (Singapore) starting November 2018.

On September 10, 2018

Speaker

정지영 (이화여대 / 부교수)


Title

'뇌 속의 벽' 허물기: 젠더, 섹슈얼리티, 그리고 지식


Abstract

여성학은 성별에 따른 차별을 없애기 위한 학문이지만, 단지 여성만을 위한 것은 아닙니다. 소수자의 입장에서 인간과 사회, 지식과 권력, 역사와 현실에 대한 새로운 관점을 찾기 위해 노력해 온 학문입니다. 이 강의에서 '남-녀'라는 이분법(젠더)과 성적인 문제들(섹슈얼리티)이 회와 문화, 정치적 맥락에서 구성된 지식임을 논의하고 그에 대한 고정관념에 질문을 던져보는 것으로 여성학에 가까워지는 시간을 가져보려고 합니다. 열린 마음으로 새로운 삶의 가능성을 자유롭게 상상해보는 시간이 되길 바랍니다.


Bio

현재 이화여자대학교 여성학과 교수로 한국여성사를 연구하고 있다. 서강대 사학과에서 조선시대 여성사전공으로 박사학위를 받았다. 성별적 구조와 인식이 만들어진 과정을 역사적으로 분석하는 한편, 주변적 여성들의 다층적 흔적을 드러내는 연구를 진행하고 있다. 저서로 <질서의 구축과 균열: 조선후기의 호적과 여성들>, <동아시아 기억의 장>(편저), <임진왜란, 동아시아 삼국전쟁>(공저) 등이 있다.

On September 17, 2018

Speaker

박민우 (라인 / 테크 에반젤리스트)


Title

소프트웨어 전문가로서 개발자외의 다른길


Abstract

소프트웨어 전문가로서의 꽃은 개발자 입니다. 하지만 소프트웨어 프로젝트가 커지고 고도화 되면서 성숙하기 위해서는 개발자이외의 소프트웨어 프로젝트를 지원하는 CI 엔지니어, 에반젤리스트, Technical PM, 세일즈엔지니어등 관련직종이 발달하게 됩니다. 개발자외의 소프트웨어 직업에 대해서 알아봅니다.


Bio

현) 라인플러스 테크 에반젤리스트
전) Realm 엔지니어, 아시아 매니저
전) 인모비 솔루션 엔지니어
전) kth 기술전략팀 에반젤리스트
전) 삼성전자 SW 소프트웨어 엔지니어
KAIST 소프트웨어 대학원 석사졸

On October 01, 2018

Speaker

한보형 (서울대 / 부교수)


Title

Real-Time Visual Tracking by Convolutional Neural Networks


Abstract

Recent tracking algorithms based on convolutional neural networks achieve impressive accuracy, and MDNet is one of the seminal works among them. However, there are still many remaining issues, especially in terms of efficiency. I present a novel real-time visual tracking algorithm based on MDNet, where feature extraction time is significantly reduced by RoIAlign operations and a novel discriminative instance embedding loss is integrated in the pretraining stage to improve accuracy. The proposed real-time MDNet runs at approximately 50 frames/second with almost same accuracy with MDNet. Contrary to many existing approaches, our algorithm works very well on various datasets without dataset sensitive parameter tuning.


Bio

Bohyung Han is currently an Associate Professor in the Department of Electrical and Computer Engineering at Seoul National University, Korea. Prior to the current position, he was an Associate Professor in the Department of Computer Science and Engineering at POSTECH, Korea and a visiting research scientist in Machine Intelligence Group at Google, Venice, CA, USA. He received the B.S. and M.S. degrees from Seoul National University, Korea, in 1997 and 2000, respectively, and the Ph.D. in Computer Science at the University of Maryland, College Park, MD, USA, in 2005. He served or will be serving as an Area Chair or Senior Program Committee member of major conferences in computer vision and machine learning including CVPR, ICCV, NIPS, IJCAI and ACCV, a Tutorial Chair in ICCV 2019, and a Demo Chair in ACCV 2014. His research group won Visual Object Tracking (VOT) Challenge in 2015 and 2016.

On October 08, 2018

Speaker

Divesh Srivastava (AT&T / Head of Database Research at AT&T)


Title

The confounding problem of private data release


Abstract

In our Big Data era, as data-driven decision making sweeps through all aspects of society, the demands to make useful data available are growing ever louder. For example, the ubiquity of GPS-enabled devices has resulted in a wealth of data about the movements of individuals and populations, which can be analyzed for useful information to aid in city and traffic planning, disaster preparedness, and so on. But the problem of releasing such data without disclosing confidential information, such as the places people visit, is a subtle and difficult one. Is “private data release” an oxymoron? This talk will delve into the motivations of private data release, explore the challenges, and outline some of the historical and recent approaches developed in response to this confounding problem.


Bio

Divesh Srivastava is the Head of Database Research at AT&T Labs-Research. He is a Fellow of the Association for Computing Machinery (ACM), the Vice President of the VLDB Endowment, and the managing editor of the Proceedings of the VLDB Endowment (PVLDB). He has served as an associate editor of the ACM Transactions on Database Systems (TODS), and as an associate Editor-in-Chief of the IEEE Transactions on Knowledge and Data Engineering (TKDE). He has presented keynote talks at several international conferences, and his research interests and publications span a variety of topics in data management. He received his Ph.D. from the University of Wisconsin, Madison, USA, and his Bachelor of Technology from the Indian Institute of Technology, Bombay, India.

On October 22, 2018

Speaker

한요섭 (연세대 / 부교수)


Title

Automata Theory and Applications


Abstract

An automaton is an abstract machine for modeling computer hardware and software. Automata theory is the study of computation models and the computational problems under these models using automata. Automata theory is closely related to formal language theory. There is a hierarchy in computational models (finite languages, regular languages, context-free languages, recursively enumerable languages and so on.) It is one of the oldest topics in computer science yet there are several new results based on automata theory. Nowadays automata are used in many applications in many different forms. We revisit some known results in automata theory and present how a simple language recognizer (i.e., automaton) is being used in several applications.


Bio

Prof Yo-Sub Han obtained his Ph.D. in computer science from HKUST in 2006. He worked as a senior researcher in Korea Institute of Science and Technology until 2009 and is currently an associate professor in the department of Computer Science at Yonsei University. His research interests include formal language theory, algorithm design and information retrieval.

On October 29, 2018

Speaker

Werner Sasse (Univ. Hamburg / 교수)


Title

Korean Culture - World Culture


Abstract

The lecture will focus on two purposes:
1) Introduction of some aspects of Korean culture in light of the conflict between traditional culture and the emerging new culture following the rapid industrial and social changes during the last two generations
2) Necessary changes in the view of Korean history in light of the ongoing process of modernization and globalization

Subsections in the presentation can be summarized as follows:
1) The connotation of the concept of "culture" in Korean and in English
2) The Crisis of Traditional Culture / Old and modern views in conflict
a) example "Three kingdoms period"
b) "5000 years of history"
c) Koreans as "mono-ethnic people": Mythical founder Dangun
3) Korean Culture, World Culture
a) Korean peoples have always incorporated immigrants
b) "multi-cultural society" international and national "multi-cultural society"
c) Korean cultural history and surrounding countries
i) Hangeul and Indian Phonology
ii) "Golden Ratio" and Sijo Chanting
iii) Korea sirhak 實學 = China shixue 實學 = Japan Jitsugaku 實學


Bio

Being the first Ph. D. holder in the newly established Korean Studies program at Bochum, he continued teaching Korean Studies in the German traditional understanding, that is, as a branch of philology. Concentrating on Middle and Old Korean languages he tried to connect Korean with Altaic language family studies. Later he turned to general culture studies, working on selected problems in historical, ethnological, and traditional poetic literature, with the aim of finding reference frames beyond the traditional borders of academic disciplines. Living in Korea since his retirement 2006, he is now fascinated by the re-invention of “traditional Korea”, where people living in cities and working in an industrial and IT-centered world give new meanings to traditions rooted in ca. 2000 years of agricultural society and that were then almost completely lost during the rapid economic development and urbanization process.

On November 05, 2018

Speaker

차미영 (KAIST / 부교수)


Title

Computational Social Science


Abstract

Social media and blogging services have become extremely popular. Every day hundreds of millions of users share conversations on random thoughts, emotional expressions, political news, and social issues. Users interact by following each other's updates and passing along interesting pieces of information to their friends. Information therefore can diffuse widely and quickly through social links. Information propagation in networks like Twitter and Facebook is unique in that traditional media sources and word-of-mouth propagation coexist. The availability of digitally-logged propagation events in social media help us better understand how user influence, tie strength, repeated exposures, conventions, and various other factors come into play in the way people generate and consume information in the modern society. Collectively, the rich data allows for computationally solving complex social science problems. In this talk, I will present several research directions towards computational social science, including rumor detection, price nowcasting, and alleviating depressive moods via social media.


Bio

Meeyoung Cha is an associate professor at the School of Computing in KAIST and a visiting professor at Facebook. Her research interests are in the analysis of complex network systems including online social networks with emphasis the spread of information, moods, and user influence. She received the best paper awards at ACM IMC 2007 for analyzing long-tail videos in YouTube and at ICWSM 2012 for studying social conventions in Twitter. Her research has been published in leading journals and conferences including PLoS One, Information Sciences, IJCAI, WWW, and ICWSM, and has been featured at the popular media outlets including the New York Times websites, Harvard Business Review’s research blog, the Washington Post, the New Scientist. Dr. Cha has worked at Facebook's Data Science Team as a Visiting Professor for a year.

On November 12, 2018

Speaker

이의웅 (NYU / PostDoc)


Title

Bridging Continuous and Discrete Optimization Through the Lens of Approximation


Abstract

Mathematical optimization is a field that studies algorithms, given an objective function and a feasible set, to find the element that maximizes or minimizes the objective function from the feasible set. While most interesting optimization problems are NP-hard and unlikely to admit efficient algorithms that find the exact optimal solution, many of them admit efficient "approximation algorithms" that find an approximate optimal solution.

Continuous and discrete optimization are the two main branches of mathematical optimization that have been primarily studied in different contexts. In this talk, I will introduce my recent results that bridge some of important continuous and discrete optimization problems, such as matrix low-rank approximation and Unique Games. At the heart of the connection is the problem of approximately computing the operator norm of a matrix with respect to various norms, which will allow us to borrow mathematical tools from functional analysis.


Bio

Euiwoong Lee is a postdoc at New York University hosted by Oded Regev and Subhash Khot, as part of the Simons Collaboration on Algorithms and Geometry. He was a research fellow at Simons Institute for the Theory of Computing, participating the Bridging Continuous and Discrete Optimization program. He received his PhD from Carnegie Mellon University in 2017, under the supervision of Prof Venkatesan Guruswami. His PhD thesis won the Edmund M. Clarke Doctoral Dissertation Award.

On November 19, 2018

Speaker

최승문 (포항공대 / 교수)


Title

Haptics and Automatic Authoring of Its Content


Abstract

Providing rich and immersive physical experiences to users has become an essential component in many computer-interactive applications, where haptics plays a centrol role. However, as with other sensory modalities, modeling and rendering good haptic experiences with plausible physicality is a very demanding task in terms of the cost associated with modeling and authoring, not to mention the cost for development. No general and wide-used solutions exist yet for that; most designers and developers rely on their in-house programs, or even worse, manual coding. This talk will introduce the basic concepts of haptics and the research conducted by the speaker in order to facilitate the authoring of haptic. The latter will consist of three parts: 1) Manual authoring paradigms for easier and faster synthesis of vibrotactile effects; 2) Automatic synthesis algorithms of vibrotactile effects from video and sound; and 3) Automatic synthesis algorithms of motion effects from from video and sound.


Bio

Seungmoon Choi, Ph.D, is a Professor of Computer Science and Engineering at Pohang University of Science and Technology (POSTECH) in Korea, also with a joint appointment of Creative IT Engineering. He received the BS and MS degrees in Control and Instrumentation Engineering from Seoul National University in 1995 and 1997, respectively, and the PhD degree in Electrical and Computer Engineering from Purdue University in 2003. His main research area is haptics, the science and technology for the sense of touch, as well as its application to various domains including robotics, virtual reality, human-computer interaction, and consumer electronics. He received a 2011 Early Career Award from the IEEE Technical Committee on Haptics. He serves/served in the editorial board of IEEE Transactions on Haptics, IEEE Robotics and Automation Letters, Presence, and Virtual Reality. He was the general co-chair of the IEEE Haptics Symposium in 2014 and 2016 and the program chair of the IEEE World Haptics Conference 2015. He was a co-chair of the IEEE Technical Committee on Haptics from 2009 to 2011. He has published more than 150 peer-reviewed international papers, 90 domestic papers, and 20 patents, with many best paper and best demonstration awards from premium international conferences. His specific research interests lie on haptic rendering and perception, both in kinesthetic and tactile aspects. His basic research has been applied to mobile devices, automobiles, virtual prototyping, and motion-based remote controllers. He is a senior member of the IEEE and a member of ACM, TCH, and Eurohaptics Society. A full CV of Dr. Choi is available for download at www.postech.ac.kr/~choism.

On November 26, 2018

Speaker

이은주 (삼성SDS / 랩장)


Title

삼성SDS AI Analytics 기술 및 사례


Abstract

AI Everywhere 시대가 도래하고 있습니다. 4차 산업혁명과 함께 AI/Analytics기술은 빠르게 확산되고 있습니다. 이러한 AI기술을 기업에서 어떻게 분류되고 연구/개발되고 있는지, AI기술을 도입하여 산업에서 어떻게 활용하여 혁신하고 있는지, 이런 과정에서 나타나는 한계점들을 나누어보고자 합니다.


Bio

現 삼성SDS 연구소 데이터분석센터 데이터분석Lab장
-Brightics 분석플랫폼 및 산업별 분석모델 개발
금융프로세스/컨설팅 전문가
-삼성생명/화재/증권, KDB, KB, NH, 무역보험공사 등

On December 03, 2018

Speaker

이봉신 (MS / Senior researcher)


Title

Data-Driven Storytelling with Expressive Visualization


Abstract

Practitioners are increasingly using visualizations to tell compelling stories supported by data, and continually developing novel techniques that integrate data visualization into a cohesive narrative. In response, those of us in the visualization research community have set to identify and refine design principles and to develop innovative techniques and tools. In this talk, I will present my recent research on data-driven storytelling, which focuses on empowering people to easily create data-driven stories leveraging expressive visualizations without the need for programming. I will also briefly discuss future research directions in this exciting field.


Bio

Bongshin Lee is a Senior Researcher at Microsoft Research. She explores innovative ways to enable people to create visualizations, interact with their data, and share data-driven stories. She has been recently focusing on helping people collect & explore the data about themselves, and share insights with others by leveraging visualizations. Bongshin currently serves as General Co-Chair for ACM ISS 2019 and Associate Editor for IEEE TVCG. She has served as General Co-Chair for IEEE PacificVis 2017 and Papers Co-Chair for IEEE InfoVis 2015 & 2016, and IEEE PacificVis 2018. She earned her MS and PhD in Computer Science from University of Maryland at College Park in 2002 and 2006, respectively.