The Summer Research Institute is an I&C Annual Event.  During this period the laboratories focus on an active exchange of research ideas with visiting scholars from renowned international institutions worldwide.  The visitors give one-hour talks on their research, accessible to a broad audience.  This year from 11th-14th June, as part of SuRI, we are organising the Algorithmic Frontiers Workshop.

Abstract :
Guardol is a domain-specific language designed to facilitate the construction of correct network guards operating over tree-shaped data. The Guardol system generates Ada code from Guardol programs and also provides speci cation and automated veri cation support.
Guard programs and specications are translated to higher order logic, then deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data.
The result is that certain complex properties of Guardol programs can be proved fully automatically.  Reasoning challenges for guards involve several aspects:
   - Reasoning about tree structured data
   - Reasoning about strings
   - Reasoning about arrays
as well as language design to easily support such reasoning.  In this talk we describe how some of these challenges have been addressed, and how several are yet to be addressed.

Bio :
Software plays an increasing role in the operation of critical systems. As these systems become more complex, ensuring software correctness becomes much more difficult. I am interested in automated formal techniques for precisely specifying, implementing, and verifying software. To support these activities, I have developed several translation and analysis tools to support formal reasoning and test case generation. I have significant experience in applying formal verification and auto-test generation techniques to production DO178B Level A and B avionics software development efforts.
I have 15 years experience in software development and analysis, including 10 years experience in Model-Based Development & safety-critical systems. Most of that time has been spent developing simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, Lustre, and RSML-e. I have led successful formal verification projects on large industrial avionics models, including displays (Rockwell-Collins ADGS-2100 Window Manager), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program). I was the lead developer of the Rockwell-Collins Gryphon tool suite, which can be used for compilation, test-case generation, and formal analysis of Simulink/Stateflow models. This tool suite has been used both for academic research and industrial verification projects.
I completed my PhD at the University of Minnesota in January, 2005.  As a graduate student, I worked in the Critical Systems Research Group ( CriSys ), where I helped design a synchronous language called Requirements State Machine Language without Events (RSML-e).  My Masters thesis provided the first complete formalization of RSML-e, written in the Z formalism. This formalization has formed the backbone of the RSML-e NIMBUS Simulator and translation tools from RSML-e to model checking and theorem proving tools.  My PhD dissertation re-formalized RSML-e using higher-order abstract syntax and structural operational semantics to create a provably-correct translator from RSML-e to a subset of C.

Abstract:
How can we make parallel programming accessible to average developers in the vast commodity applications arena? I will argue that "deterministic-by-default" parallel programming models are part of the answer. With such a model, the programmer is freed from the burden of reasoning about thread interleavings, data races, deadlock, or the intricacies of memory models.  Unfortunately, this goal is challenging to achieve for modern imperative, object-oriented languages. I will describe Deterministic Parallel Java, a deterministic-by-default parallel programming language that guarantees sequential semantics (except where requested otherwise) for explicitly parallel programs.  The deterministic guarantees are achieved using a region-based type and effect system that is a simple extension to base Java. Programmers can combine nondeterministic algorithms with deterministic ones in a data race-free, isolated, manner, with the strongest safety guarantees of any parallel language or system. DPJ also supports the safe use of expressive parallel frameworks.  An interactive tool called DPJizer, under development, enables programmers to port existing Java code to DPJ semi-automatically. We are now exploring how these techniques can be extended to C++, combined with existing parallel languages such as Cilk++ or OpenMP, and applied to large, industrial code bases.

Bio:
Vikram Adve is a Professor of Computer Science at the University of Illinois at Urbana-Champaign. His research interests include compilers and programmming languages, and their use for improving software productivity, security and reliability.  His research group developed the LLVM Compiler Infrastructure, a widely distributed and novel compiler framework for 'lifelong' optimization of programs. LLVM is in production use by several companies including Apple, Adobe, Cray, and others, and has replaced GCC as the primary compiler on both iOS 5 and MacOS X. LLVM is also used by a large number of open source projects and research groups.  Adve has been Associate Editor of ACM TOPLAS and Program Chair or Co-chair for ASPLOS, VEE, and LCPC. Adve has  also received the NSF CAREER award, the UIUC Computer Science Department's Outstanding Junior Faculty Award, and paper awards at several conferences including PLDI, SOSP and ICSE, among others.

Abstract:
The ability to capture, manage and query workflow provenance is increasingly important for scientific as well as business applications. However provenance is a double-edged sword:   Providing complete information in response to provenance queries may not only be overwhelming for the user, but may reveal confidential information.  In this talk, we discuss the use of provenance views to alleviate these problems, and show how they can be used to address privacy concerns as well as to provide varying levels of provenance information, from fine-grained, database-style information to coarse-grained workflow-style information.  We also discuss how provenance queries can be efficiently processed over provenance views.

Bio:
Susan B. Davidson received the B.A. degree in Mathematics from Cornell University, Ithaca, NY, in 1978, and the M.A. and Ph.D. degrees in Electrical Engineering and Computer Science from Princeton University, Princeton NJ, in 1980 and 1982. Dr. Davidson is the Weiss Professor and Chair of Computer and Information Science at the University of Pennsylvania, where she has been since 1982.
Dr. Davidson's research interests include database and web-based systems, scientific data management, and "big data". She co-developed the Kleisli data integration system (with Drs. Buneman, Tannen, Overton, and Wong), which was used for on-the-fly data integration of large genomic datasets. She has also developed techniques for provenance management in scientific workflow systems, including support for search and query, techniques for focusing user attention on "relevant'' provenance information, and marrying database-style and workflow-style provenance management using Pig-Latin to elucidate the function of black-box modules. More recently, she has focused on privacy concerns surrounding the capture and use of provenance information in both databases and workflow systems.
Dr. Davidson was the founding co-director of the Penn Center for Bioinformatics from 1997-2003, and the founding co-director of the Greater Philadelphia Bioinformatics Alliance. She holds a secondary appointment in the Department of Genetics, is an ACM Fellow, received the Lenore Rowe Williams Award (2002), and was a Fulbright Scholar and recipient of a Hitachi Chair (2004). She currently serves on the VLDB Executive Committee, the CRA Board, and is a member of the CCC Council.

Abstract:
For at least two thousand years, voting has been used as one of the most effective ways to aggregate people’s ordinal preferences.
In the last 50 years, the rapid development of Computer Science has revolutionize every aspect of the world, including social choice (voting); and meanwhile, social choice has also found applications in many fields in Computer Science, including multiagent systems, recommendation systems, and crowdsourcing. This motivates us to study (1) conceptually, how computational thinking changes the traditional theory of voting, and (2) methodologically, how to better use voting for preference/information aggregation with the help of Computer Science.
In this talk, I will briefly discuss two research directions, one for each question asked above. The first focuses on investigating how computational thinking affects the game-theoretic aspects of voting. I will discuss the rationale and possibility of using computational complexity to protect voting from a type of strategic behavior of the voters, called manipulation. The second studies a voting setting called Combinatorial Voting, where the set of alternatives is exponentially large and has a combinatorial structure. I will focus on the design and evaluation of novel mechanisms for combinatorial voting that balance computational efficiency and the expressivity of the voting language, in light of some recent developments in Artificial Intelligence.

Short bio:
Lirong Xia is a postdoctoral fellow at the Center for Research on Computation and Society at Harvard University. He got a Ph.D. in Computer Science in 2011  and an M.A. in Economics in 2010, both from Duke University. His research focuses on the intersection of computer science and microeconomics, in particular computational social choice, game theory, mechanism design, and prediction markets.

Abstract:
Several studies have documented the constantly evolving privacy practices of social networking sites and users' misunderstandings about them. Justifiably, users have
criticized the interfaces to "configure" their privacy preferences as opaque, disjointed, uninformative and ultimately ineffective. The same problems have also plagued the
constantly growing economy of third-party applications and their equally troubling authentication and authorization dialogues with important options being unavailable
at installation time and/or widely distributed across the sites' privacy options pages.
In this talk, I will discuss the results of a field study of the current authorization dialogue for the currently dominant social networking site as well as four canonical designs of installation dialogues which are based on the internationally favored Fair Information Practice Principles (FIPPs). In particular, we study and document the effectiveness of installation-time configuration and awareness-enhancing interface changes when 250 users investigate our experimental application in the privacy of their homes.

Bio:
Dr. Grossklags is an Assistant Professor at the College of Information Sciences and Technology at the Pennsylvania State University. He is affiliated with the Security and Risk Analysis program and a member of the steering committee of the Center for the Study of Global Financial Stability. Previously, he served as a Postdoctoral Research Associate at the Center for Information Technology Policy, and as a Lecturer of Computer Science at Princeton University. In 2009, he completed his doctoral dissertation at UC Berkeley's School of Information. While at UC Berkeley, he also obtained master's degrees in Computer Science, and Information Management and
Systems.
He is studying information privacy, security, technology policy and networked interactions from a theoretical, empirical and practical perspective. Specifically,
Dr. Grossklags is motivated to contribute to a better understanding of the current and future marketplace for personal and corporate information, and improved designs of the underlying evolving security infrastructure. His academic work is very cross-disciplinary and utilizes analytic, empirical and experimental methodologies.

Abstract:
Information of interest may be found on the Web in a variety of forms, in many systems, and with different access protocols. A typical user may have information on many devices (smartphone, laptop, TV box, etc.), many systems (mailers, blogs, Web sites, etc.), many social networks (Facebook, Picasa, etc.). This same user may have access to more information from family, friends, associations, companies, and organizations. Today, the control and management of the diversity of data and tasks in this setting are beyond the skills of casual users. Facing similar issues, companies see the cost of managing and integrating information skyrocketing.
We are interested here in the management of such data. Our focus is not on harvesting all the data of a particular user or a group of users and then managing it in a centralized manner. Instead, we are concerned with the management of Web data in place in a distributed manner, with a possibly large number of autonomous, heterogeneous systems collaborating to support certain tasks.
Our thesis is that managing the richness and diversity of user-centric data residing on the Web can be tamed using a holistic approach based on a distributed knowledge base. All Web informations are represented as logical facts, and Web data management tasks as logical rules. We discuss Webdamlog, a variant of datalog for distributed data management that we use for this purpose. The automatic reasoning povided by its inference engine, operating over the Web knowledge base, greatly benefits a variety of complex data management tasks that currently require intense work and deep expertise.
This work is part of the Webdam ERC project.

Bio:
Serge Abiteboul, Telecom Paris, PhD computer science, USC Los Angeles, and Thèse d’Etat, University of Paris Sud. He has held professor positions at Stanford and Ecole Polytechnique. He is one of the co-authors of Foundations of Databases, and, recently, of Web Data Management. He co-founded in 2000 a start-up, named Xyleme. He received the 1998 ACM SIGMOD Innovation Award. He has been program chair of a number of conferences including ACM PODS-95, ICALP-94, ICDT-90, ECDL-99 and VLDB-09, ICDE-11, track of WWW-12. He has been awarded in 2008 an ERC Advanced Grant, namely Webdam, on Foundations of Web Data Management. He is a member of the French Academy of Sciences since 2008.

Abstract:
One of the most important analyses on human DNA sequences is read mapping, which aligns a large number of short DNA sequences (called reads) produced by sequencers to a reference human genome. The analysis involves intensive computation (calculating edit distances over millions upon billions of sequences) and therefore needs to be outsourced to low-cost commercial clouds. This asks for scalable privacy preserving techniques to protect the sensitive information sequencing reads contain. Such a demand cannot be met by the existing techniques, which are either too heavyweight to sustain data-intensive computations or vulnerable to re-identification attacks. In this talk, I describe a new technique that makes an important step towards secure and scalable read mapping on the hybrid cloud, which includes both the public commercial cloud and the private cloud within an organization. Inspired by the famous “seed-and-extend” method, our approach strategically splits a mapping task: the public cloud seeks exact matches between the keyed hash values of short read substrings (called seeds) and those of reference sequences to roughly position reads on the genome; the private cloud extends the seeds from these positions to find right alignments. Our novel seed-combination technique further moves most workload of this task to the public cloud. The new approach is found to work effectively against known inference attacks, and also easily scale to millions of reads.

Bio:
Dr. XiaoFeng Wang is an associate professor in the School of Informatics and Computing at Indiana University, Bloomington. He received his Ph.D. in Electrical and Computer Engineering from Carnegie Mellon University in 2004, and has since been a faculty member at IU. Dr. Wang is a recognized active researcher on system, network and data security. His group extensively publishes at leading security venues and vigorously pursues innovative and high-impact research directions.  His current work focuses on privacy issues in processing and dissemination of human genome data and security/privacy issues in Cloud Computing. He is a recipient of 2011 Award for Outstanding Research in Privacy Enhancing Technologies (the PET Award) and the Best Practical Paper Award at the 32nd IEEE Symposium on Security and Privacy. His work frequently receives attentions from the media, including CNN, MSNBC, Slashdot, CNet, PC World, etc.. Dr. Wang has also been actively serving the research community, participating in the program/organization committees of numerous conferences/workshops. His research is supported by the NSF, Department of Homeland Security, the Air Force and Microsoft Research. He was the director for the Security Informatics program including the Master Program in Security at IU in 2010.

Abstract:
I shall discuss recent work (much of it joint with biologists Adi Livnat and Marcus Feldman) on some central problems in Evolution that was inspired and informed by computational ideas. Considerations about the performance of genetic algorithms led to a novel theory on the role of sex in Evolution based on the concept of mixability. And a natural random process on Boolean functions can help us understand better Waddington's genetic assimilation phenomenon, in which an acquired trait becomes genetic, and the emergence of a trait in a population in the absence of mutation.

Bio:
I studied in Athens Polytechnic (BS in EE 1972) and Princeton (MS in EE, 1974 and PhD in EECS, 1976).
Since then, I have taught at Harvard, MIT, Athens Polytechnic, Stanford, and UCSD.
I came to Berkeley in January 1996 (but I was here also in 1978 as a Miller fellow).
I am interested in the theory of algorithms and complexity, and its applications to databases, optimization, AI, networks, game theory, and evolution.

Abstract:
Location systems are key to a rich experience for mobile users. When they roam outdoors, mobiles can usually count on a clear GPS signal for an accurate location, but indoors, GPS usually fades, and so up until recently, mobiles have had to rely mainly on rather coarse-grained signal strength readings for location. What has changed
this status quo is the recent trend of dramatically increasing numbers of antennas at the indoor AP, mainly to bolster capacity and coverage with multiple-input, multiple-output (MIMO) techniques. In the near future, the number of antennas at the access point will increase to meet increasing demands for wireless capacity with MIMO links, spatial division multiplexing, and interference management.  We thus observe an opportunity to revisit the important problem of localization with a fresh perspective.  I will talk about the design and experimental evaluation of ArrayTrack, an indoor location system that uses Angle-of-Arrival information at access points to track wireless clients in real time as they roam about a building. We have prototyped ArrayTrack on the WARP platform, emulating the capabilities of an inexpensive 802.11 wireless access point. Our results show that ArrayTrack can pinpoint 33 clients spread out over an indoor office environment to within a median 36 cm location accuracy.
Joint work with Jie Xiong.

Bio:
Kyle Jamieson is a Lecturer in the Networks research group at University College London. His research interests are in building real-world wireless systems that cut across the boundary of digital communications and networking. He received the PhD in June 2008 from the Massachusetts Institute of Technology (Cambridge, Massachusetts) and is PI on a European Research Council "Ideas" Programe Research Fellowship.