Grad Seminar Guest: Niki Vazou

Graduate seminar, Thursday, Oct. 13, 4:30-5:30, POST 126

LiquidHaskell: Liquid Types for Haskell

Niki Vazou, University of California, San Diego


Code deficiencies and bugs constitute an unavoidable part of software systems. In safety-critical systems, like aircrafts or medical equipment, even a single bug can lead to catastrophic impacts such as injuries or death. Formal verification can be used to statically track code deficiencies by proving or disproving correctness properties of a system. However, at its current state formal verification is a cumbersome process that is rarely used by mainstream developers.

This talk presents LiquidHaskell, a usable formal verifier for Haskell programs. LiquidHaskell naturally integrates the specification of correctness properties in the development process. Moreover, verification is automatic, requiring no explicit proofs or complicated annotations.  At the same time, the specification language is expressive and modular, allowing the user to specify correctness properties ranging from totality and termination to memory safety and safe resource (e.g., file) manipulation.  Finally, LiquidHaskell has been used to verify more than 10,000 lines of real-world Haskell programs.

LiquidHaskell serves as a prototype verifier in a future where formal techniques will be used to facilitate, instead of hinder, software development. For instance, by automatically providing instant feedback, a verifier will allow a web security developer to immediately identify potential code vulnerabilities.


Niki Vazou is a Ph.D. candidate at University of California, San Diego, supervised by Ranjit Jhala. She works in the area of programming languages, with the goal of building usable program verifiers that will naturally integrate formal verification techniques into the mainstream software development chain. Niki Vazou received the Microsoft Research Ph.D. fellowship in 2014 and her BS from National Technical University of Athens, Greece in 2011.

ICS Lunch and Seminar Series: Michael Goodrich

POST318B (ICSpace) Thursday September 8, 12:00pm
Pizza and beverages provided!

Invertible Bloom Lookup Tables and Their Applications to Data Analysis

Michael Goodrich, Ph.D.

We present a version of the Bloom filter data structure that supports not only the insertion, deletion, and lookup of key-value pairs, but also allows a complete listing of the pairs it contains with high probability, as long the number of key-value pairs is below a designed threshold. Our structure allows the number of key-value pairs to greatly exceed this threshold during normal operation. Exceeding the threshold simply temporarily prevents content listing and reduces the probability of a successful lookup. If entries are later deleted to return the structure below the threshold, everything again functions appropriately. We also show that simple variations of our structure are robust to certain standard errors, such as the deletion of a key without a corresponding insertion or the insertion of two distinct values for a key. The properties of our structure make it suitable for several applications, including database and networking applications that we highlight.

Prof. Goodrich received his B.A. in Mathematics and Computer Science from Calvin College in 1983 and his PhD in Computer Sciences from Purdue University in 1987. He is a Chancellor’s Professor at the University of California, Irvine, where he has been a faculty member in the Department of Computer Science since 2001. Dr. Goodrich’s research is directed at the design of high performance algorithms and data structures with applications to information assurance and security, the Internet, machine learning, and geometric computing. With over 300 publications, including several widely-adopted books, his recent work includes contributions to efficient and secure distributed data structures, information privacy, social networks, and cloud security. He is an ACM Distinguished Scientist, a Fellow of the American Association for the Advancement of Science (AAAS), a Fulbright Scholar, a Fellow of the IEEE, and a Fellow of the ACM. He is a recipient of the IEEE Computer Society Technical Achievement Award, the Brown Univ. Award for Technological Innovation, and the Pond Award for Excellence in Undergraduate Teaching.

Grad Seminar Guest: Chris Zimmerman

Graduate seminar, Thursday, Sept. 8, 4:30-5:30, POST 126

Space vs. Place: Comparing Space-based Movements and Place-based Experiences while Exploring the Digital Reverberations of City Spaces and Public Places

Chris Zimmerman, Copenhagen Business School

Abstract  This research applies urban informatics methods and techniques on big data generated from the concentrated environment of the second largest music festival in the world, Roskilde Festival. First, we explain how to utilize relevant dimensions from human geography theories towards mapping a ‘Geography of Importance’. Second, we elaborate on methods deployed for collecting both mobile GPS and social media traces that the smart phone generates in physical spaces. Third, we compare and contrast the automatically geocoded presence in space and at events with the intentionally socially tagged consumption of these spaces and events as place-based experiences. In doing so, these two layers of space-based movements and place-based experiences reveal the appropriation of affordances and choices of aesthetic appreciation by the crowd at large of what is subjectively and relatively meaningful, actionable, and valuable.

Seminar: Terence Parr, “Mini-tutorial on building ANTLR 4 grammars”

Programmers run into parsing problems all the time, whether it’s a data format like JSON, a network protocol like SMTP, a server configuration file for Apache, or a simple spreadsheet macro language. My goal with ANTLR 4 was to make it as easy as possible to build parsers and the language applications on top. ANTLR will accept all grammars (minor caveat: no indirect left-recursion) and can produce extremely efficient ALL(*), Adaptive LL(*), parsers. In this talk, I’ll give a mini-tutorial on ANTLR 4 and the Intellij plugin.

Thursday, March 17th, 4:30pm-5:30pm in POST 126

Bio: Terence Parr is a professor of computer science at the University of San Francisco where he continues to work on his ANTLR parser generator. Until January 2014, Terence was the graduate program director for computer science and was the founding director of the MS in Analytics program. Before entering academia in 2003, he worked in industry and co-founded Terence herded programmers and implemented the large jGuru developers website, during which time he developed and refined the StringTemplate engine. Terence has consulted for and held various technical positions at companies such as Google, IBM, Lockheed Missiles and Space, NeXT, and Renault Automation. Terence holds a Ph.D. in Computer Engineering from Purdue University.

Seminar, Alex Cabello, “Introduction to AlgorithmHub and the Technology Behind the Platform”

AlgorithmHub is a cloud based service that promotes the development, sharing and publishing of algorithms. AlgorithmHub creates communities around algorithms, thus minimizing reinvention and accelerating the adoption of algorithms. During the seminar we will provide a brief tutorial of AlgorithmHub and some of the open source technologies behind the platform, including Docker, Node, and React. Please bring a computer if you would like to follow along with the tutorial.

Thursday, Feb 25th, 4:30pm5:30pm in POST 126.

Bio: Alex Cabello is a founder of AlgorithmHub, which is a recent graduate from XLR8UH. He is a UH alumnus.

Seminar: Riko Jacob, IT University of Copenhagen, “Sparse Grids and the I/O-Model: How Theory Helps”

Starting from the observation that quite frequently the memory system is the performance bottleneck, I will discuss a typical memory efficient algorithm, namely the classical one for dense matrix multiplication. Then I will briefly sketch how similar ideas are helpful in the setting of Sparse Grids (I’ll explain what that is too), and report on experiments we did with this memory efficient algorithm.

Thursday, Feb 18, 2016, 4:30pm-5:30pm in POST 126

Bio: Dr. Jacob is Associate Professor for Algorithm Engineering in the Theoretical Computer Science Section of IT University of Copenhagen, where he is a member of the Algorithms Group.

In 1997 Dr. Jacob received his Diploma in Computer Science in Warzburg (Germany) and in 2002 his PhD from Aarhus University (Denmark). He has worked as a researcher at Los Alamos National Lab (USA), LMU Munich (Germany), TU Munich (Germany), and ETH Zurich (Switzerland).

Seminar, Pourang Irani, “Toward ubiquitous analytics”

Our reliance on data for making decisions, or data analytics, is undergoing a transformation from being predominantly carried out by a single individual or a group of experts, and in limited settings (such as on traditional PCs) to taking place while on-the-go and in the field of action. Data analytics is becoming necessary for the general end-user. For example, an athlete may consult their network of body-worn sensors to gauge their training performance, a shopper may need to quickly consult web sites of competing products as well as their personal finances before making a purchase, or a parent may track information about their child’s performance, over time, in school. Common among all these scenarios is the growing need for advanced tools that will enable end-users to interact with vast and diverse amounts of data for sense-making, while on-the-go. However current tools and devices, such as smartphones and head-worn displays, are not tailored to enable the need for interacting with large or diverse data sets.

In this talk I will present on-going work in ubiquitous analytics, that focuses on the development of end-user software interface technologies for meeting data analytic needs in varied, ad-hoc mobile environments. Such tools will facilitate the advanced exploration and interaction with data, ‘anytime’ and ‘anywhere’, through improved information navigation, visualization and manipulation interfaces on potentially information-rich portals such as mobile and wearable devices. I will present recent examples from work in our lab on Ubiquitous Analytics, and open a discussion of potential projects that fall under this umbrella of research activity.

BIO: Pourang Irani is a Professor in the Department of Computer Science at the University of Manitoba and Canada Research Chair in Ubiquitous Analytics. His research is in the areas of Human-Computer Interaction and Information Visualization. More specifically, his work concentrates on designing and studying novel interaction methods and systems for giving end-users efficient access to various information structures (maps, spatio-temporal data and video) on a variety of computing devices (smartphones, wearable devices and large shared surfaces). This has placed his research at the core of Ubiquitous Analytics, a field he is pioneering, and which concerns the development of interactive and visualization tools for exploring information “anywhere” and “anytime”.

Jan 26 at 1pm in Keller 102

Seminar: Dusko Pavlovic, “On the Unreasonable Ineffectiveness of Security Engineering: Adverse Selection of Trust Certificates

In his famous 1960 essay, Eugene Wigner raised the question of “the unreasonable effectiveness of mathematics in natural sciences”. After several decades of security research, we are able to ask similar questions about security: Do the security technologies make us more secure? Is security engineering not unreasonably ineffective?

As a case to the point, I describe the phenomenon of adverse selection of trust certificates. According to several empiric studies, a web merchant with a trust certificate is roughly twice as likely to be a scammer as a web merchant without a trust certificate. While the phenomenon could be attributed to a lack of diligence, and even to conflicts of interest in trust authorities, a model that I shall present suggests that public trust networks would remain attractive targets for spoofing even if trust authorities were perfectly diligent. The reason is that trust is like money: the rich get richer. The methods to mitigate the resulting vulnerability are analyzed in the extensions of the model.

Bio: Dusko Pavlovic was born in Sarajevo, studied mathematics in Utrecht and Cambridge, and worked at McGill, before turning to computer science at Imperial College London. He left academia in 1999 and worked in Silicon Valley for 10 years. He gradually returned to academia, first as a Visiting Professor at Oxford 2007-2012, then as Professor of Security at Twente 2010-2013. He held a Chair in Information Security at Royal Holloway University of London 2010-2014, where graduate degrees in security have been given since 1992. There he founded the Adaptive Security and Economics Lab (ASECOLab), hosting joint projects with some of the founders and luminaries of modern cryptography. Since 2014, Dusko and several members of ASECOLab have been at University of Hawaii at Manoa, where they launched the Security Science (SecSci) Focus Area, while initiating 4 new research projects in cyber security strategies.

Date: Thursday, January 14, 2016

Time: 11am – 12pm

Location: Holmes Hall 389

Seminar: Alan Mislove, “Measuring personalization of online services”

Today, many web services personalize their content, including Netflix (movie recommendations), Amazon (product suggestions), and Yelp (business reviews). In many cases, personalization provides advantages for users: for example, when a user searches for an ambiguous query such as “router,” Amazon may be able to suggest the woodworking tool instead of the networking device.  However, personalization is rarely transparent (or even labeled), and has the potential be used to the user’s disadvantage.  For example, on e-commerce sites, personalization could be used to manipulate the set of products shown (price steering) or by customizing the prices of products (price discrimination).  Unfortunately, today, we lack the tools and techniques necessary to be able to detect when personalization is occurring, as well as what inputs are used to perform personalization.

In this talk, I discuss my group’s recent work that aims to address this problem.  First, we develop a methodology for accurately measuring when web services are personalizing their content.  While conceptually simple, there are numerous details that our methodology must handle in order to accurately attribute differences in results to personalization (as opposed to other sources of noise).  Second, we apply this methodology to two domains:  Web search services (e.g., Google, Bing) and e-commerce sites (e.g.,, Expedia).  We find evidence of personalization for real users on both Google search and nine of the popular e-commerce sites.  Third, using fake accounts, we investigate the effect of user attributes and behaviors on personalization; we find that the choice of browser, logging in, and a user’s previously content can significantly affect the results presented.

Bio: Alan Mislove is an Associate Professor at the College of Computer and Information Science at Northeastern University.  He received his Ph.D. from Rice University in 2009. Prof. Mislove’s research concerns distributed systems and networks, with a focus on using social networks to enhance the security, privacy, and efficiency of newly emerging systems.  He is a recipient of an NSF CAREER Award (2011), and his work has been covered by the Wall Street Journal, the New York Times, and the CBS Evening News.

Time: 3-4PM on Wednesday, January 13, 2016

Place:POST 126

Seminar: Hendranus Vermeulen, “The gamification of computer science”

The talk introduces the terms ‘serious games’ and ‘gamification’, which derive from the troublesome concept ‘game’. It focuses on the gamification of the 2nd year Computer Game Design course, which was developed and coordinated from 2012 to 2015 at the Department of Computer Science, University of Cape Town. The design and research methods, results and findings are discussed. This discussion highlights opportunities and challenges for the gamification of Computer Science courses; in particular the contradiction between the cultures of academia and games, which has transformative potential.

Bio: Hendranus Vermeulen is a postdoctoral research fellow at the Department of Computer Science, University of Cape Town. He is investigating serious games and gamification with particular emphasis on evaluating and enhancing learning activities in games design and artificial intelligence. He develops educational theory, methodology and tools through practice in digital media, virtual reality, games and simulations. His PhD thesis developed a methodology for the design and evaluation of learning in virtual worlds.

Wednesday, January 13, 2016
POST 302 10:30am-11:30am