ICS Lunch and Seminar Series: Pawel Sobocinski on 11/3

Pawel Sobocinski

Where and When: POST318B (ICSpace) Thursday November 3, 12:00pm

Title: Compositional model checking of concurrent systems with Petri nets


Compositionality and process equivalence are both standard concepts of process algebra. Compositionality means that the behaviour of a compound system relies only on the behaviour of its components, i.e. there is no emergent behaviour. Process equivalence means that the explicit statespace of a system takes a back seat to its interaction patterns: the information that an environment can obtain though interaction. Petri nets are a widely used and understood, model of concurrency. Nevertheless, they have often been described as a non-compositional model, and tools tend to deal with monolithic, globally-specified models. In this talk I will introduce Petri Nets with Boundaries (PNB), which is a compositional, graphical algebra of elementary net systems, an important class of Petri nets. I will show that compositionality and process equivalence are a powerful combination that can be harnessed to improve the performance of checking reachability and coverability in several common examples where Petri nets model realistic concurrent systems. 


Pawel Sobocinski studied computer science and mathematics at the University of Sydney, Australia and completed his PhD at the University of Aarhus, Denmark, in 2004. He has held postodoctoral positions at the Universities of Pisa, Paris VII and Cambridge, and, since 2007, an academic position at the University of Southampton, UK. His research interests lie in concurrency theory, verification, programming languages, and applications of category theory in computer science. 

ICS Lunch and Seminar Series: Bas Westerbaan on 10/13

Bas Westerbaan

Where and When: POST318B (ICSpace) Thursday October 13, 12:00pm

Title: In search for the smallest Kochen-Specker system


At the heart of the famous Conway-Kochen Free Will Theorem and Kochen and Specker’s argument against non-contextual hidden variable theories is the existence of a Kochen-Specker (KS) system: a finite set of points on the sphere that is not “010-colorable”.  The first KS-system was found in 1975 consisting of 117 points.  In 1991 Penrose and Peres independently found a system of 33 points.  Around 1995 John Conway took the lead with his 31 point system.  To this day, Conway’s system is the smallest known Kochen-Specker system.  In public lectures Conway encouraged the search for a smaller system.

In 2009 Arends, Ouaknine and Wampler from Oxford have shown that a Kochen-Specker system must have at least 18 points.  They did this by reducing the problem to the existence of graphs with a topological embeddability and non-colorability property.  The bottleneck in their search proved to be enumerating the sheer number of graphs on more than 17 vertices and deciding embeddability.

Continuing their effort, we reduced the class of graphs to consider and found a more practical algorithm to decide embeddabiltiy.  This allowed us to show that a Kochen-Specker system must have at least 22 points.

There is a lot of room for improvement; e.g. if the enumeration of graphs can be effectively restricted to those graphs in which every point is part of a triangle, the upper bound may be pushed to 24 and the smallest KS-system might be found. So, if you have a knack for algorithms, please join and give this problem a shot!


Sander Uijlen and Bas Westerbaan. “A Kochen-Specker system has at least 22 vectors.” New Generation Computing 34.1-2 (2016): 3-23.


Bas Westerbaan is Ph.D-student at Radboud Universiteit Nijmegen (the Netherlands).

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.

Director of Grease delivers lecture on 360 film making

October 5, 2016

Known for directing films such as Grease, The Blue Lagoon, Flight of the Navigator, and Honey I Blew Up the Kids, Randal Kleiser visits the Laboratory for Advanced Visualization and Applications to deliver an Academy for Creative Media Master Series lecture on 360 film production. The lecture was delivered as part of Professor Jason Leigh’s Virtual Reality and Augmented Reality class.

Kleiser spoke of his experiences in directing the 360 short film: Defrost, based on a script he had written before producing Grease in 1987. In addition the students treated him to demonstrations of their latest VR and AR creations.

Defrost is a sci-fi screen play about cryogenic life extension where a woman gets woken up from decades of sub-zero temperature suspension, to find herself confronted with a much older family, and a nagging suspicion that some things just don’t feel right.

In the film, the viewer plays as the protagonist and experiences it using a virtual reality headset such as the HTC Vive or Oculus.

Randal Kleiser

LAVA demonstrates satellite visualization at AMOS 16

The 17th Annual Advanced Maui Optical and Space Surveillance Technologies Conference was held on Sept. 20-23, 2016 at the Wailea Marriott Resort and Spa with a record-breaking attendance of over 680 participants.

Representing the  Laboratory for Advanced Visualization & Applications, two undergraduate students Ryan Theriot, who is studying Computer Science, and Andrew Guagliardo who is studying Animation with the Academy for Creative Media exhibited a program developed by Theriot called SatWatch at the conference.

SatWatch is a virtual reality exploration of satellite orbits around Earth. By pulling publicly available TLE (Two-Line element) data from the Celestrak website, SatWatch is able to create a predictive model of orbits for a wide variety of satellites. The TLE dataset is converted using the OrbitTools library. The entire program is built in the Unity game engine, a popular tool for developing interactive applications. For hardware, SatWatch utilizes the HTC Vive, which allows a user to interact with the virtual, 3d environment using motion tracking. This combination creates a natural way for users to explore the data in an immersive experience. SatWatch is an example of a complex dataset represented in an intuitive way, allowing users to easily understand satellite orbits in an interactive visualization environment.


Town Hall Meeting between ICS Faculty and Students


Students participating on the Town Hall meeting.

ICS faculty and students held a “town hall” meeting in ICSpace to discuss issues. Among the topics discussed were the “no repeat” policy for introductory classes, the “B-or-better” policy in introductory classes for majoring in ICS, the availability of writing intensive and oral intensive courses within ICS, class scheduling, and changes on the prerequisite structure.

Faulty members also introduced themselves to students and highlighted their research.


Faculty participating in the Town Hall meeting.

Beyond issues of the curriculum, the most lively discussion ensued around the question of why a student should pursue a degree in computer science instead of some kind of technical certification from a programming bootcamp. This is a complex issue that deserves thought, and we were happy to explore it.

Oh, and there was pizza.

Many thanks to the students and faculty who participated. A special mahalo to the Academic Advising staff who also participated.



Academic counselors participated in the Town Hall meeting.


Missed it?  We will be having regular meetings of this type as long as students keep showing up.

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.

First Disrupt Army Hackathon Coming Up

Disrupt Army Hackathon

The first of a series of Web Application Hackathons will be held on Sept. 30 – Oct. 1 at the Manoa Innovation Center.

All students (17+) are welcome to join. For your hacking efforts there will be food, drinks and prizes!

“@disruptarmy disrupts information systems by hosting hackathon events for students…”

More information: http://www.disruptarmy.com/



ACM Student Chapter hosts high school events

The UH ACM Student Chapter (ACManoa) hosted two outreach workshops in ICSpace (POST 318B) earlier this month. The workshops provided students from the UH Information and Computer Science (ICS) program with the opportunity to mentor high school students interested in programming. Members of ACManoa took the opportunity to give back to the community and foster interest in the ICS program at the University.

For more details, see this posting.