WSDM will take place in Los Angeles (CA, USA) in February 2018.
WSDM will take place in Los Angeles (CA, USA) in February 2018.
A doctoral degree in computer science or related areas and an outstanding research record (commensurate for the applicant's career stage) are required. Successful candidates are expected to build a team and pursue a highly visible research agenda, both independently and in collaboration with other groups.
MPI-SWS is part of a network of over 80 Max Planck Institutes, Germany's premier basic-research organisations. MPIs have an established record of world-class, foundational research in the sciences, technology, and the humanities. The institute offers a unique environment that combines the best aspects of a university department and a research laboratory: Faculty enjoy full academic freedom, lead a team of doctoral students and post-docs, and have the opportunity to teach university courses; at the same time, they enjoy ongoing institutional funding in addition to third-party funds, a technical infrastructure unrivaled for an academic institution, as well as internationally competitive compensation.
The institute is located in the German cities of Saarbruecken and Kaiserslautern, in the tri-border area of Germany, France, and Luxembourg. We maintain an international and diverse work environment and seek applications from outstanding researchers worldwide. The working language is English; knowledge of the German language is not required for a successful career at the institute.
Qualified candidates should apply on our application website (apply.mpi-sws.org). To receive full consideration, applications should be received by December 1st, 2017.
The institute is committed to increasing the representation of minorities, women, and individuals with physical disabilities. We particularly encourage such individuals to apply. The initial tenure-track appointment is for five years; it can be extended to seven years based on a midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.
NIPS will take place in Long Beach (CA, USA) in December 2017.
"Derek Dreyer has made deep, creative research contributions of great breadth. His areas of impact are as diverse as module systems, data abstraction in higher-order languages, mechanized proof systems and techniques, and concurrency models and semantics. He has refactored and generalized the complex module systems of SML and OCaml; devised logical relations and techniques that enabled advances in reasoning about higher-order imperative programs; and developed novel separation logics for modular verification of low-level concurrent programs. His research papers are a model of clarity and depth, and he has worked actively to translate his foundational ideas into practice – most recently with the RustBelt project to provide formal foundations for the Rust language. Additionally, Dreyer has contributed leadership, support, and mentorship in activities such as the PLMW series of workshops, which are instrumental in growing the next generation of PL researchers."
Previous recipients of the award have included Stephanie Weirich, David Walker, Sumit Gulwani, Lars Birkedal, and Shriram Krishnamurthi.
The award citation reads as follows: "This is one of the first papers that examine multiple online social networks at scale. By introducing novel measurement techniques, the paper has had an enduring influence on the analysis, modeling and design of modern social media and social networking services."
RTSS 2017 will be held from December 6 to December 8 in Paris, France.
Amaury Pouly's thesis shows that problems which can be solved with a computer in a reasonable amount of time (more specifically problems which belong to the class P of the famous open problem “P = NP?”) can be characterized as polynomial length solutions of polynomial differential equations. This result paves the way for reformulating certain questions and concepts of theoretical computer science in terms of ordinary polynomial differential equations. It also revisits analog computational models and demonstrates that analog and digital computers actually have the same computing power, both in terms of what they can calculate (computability) and what they can solve in reasonable (polynomial) time.
PLDI 2017: Repairing Sequential Consistency in C/C++11, by Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer.
ECOOP 2017: Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris, by Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis.
Adish Singla is joining us from ETH Zurich, where he has completed his Ph.D. in computer science. His research focuses on designing new machine learning frameworks and developing algorithmic techniques, particularly for situations where people are an integral part of computational systems. Adish joins the institute as a tenure-track faculty member, effective Oct 1, 2017.
Before starting his Ph.D., he worked as a Senior Development Lead in Bing Search for over three years. Adish received his Bachelor's degree from IIT Delhi and his Master's degree from EPFL. He is a recipient of the Facebook Fellowship in the area of Machine Learning, the Microsoft Research Tech Transfer Award, and the Microsoft Gold Star Award.
Maria joins MPI-SWS from the University of Kent, England, where she is a Lecturer at the School of Computing. She was previously a postdoctoral researcher at Microsoft Research Redmond. Maria received her Ph.D. from the Department of Computer Science of ETH Zurich and was awarded with the ETH medal and the EAPLS Best PhD Dissertation Award. She completed her Bachelor’s and Master’s degrees at the Department of Electrical and Computer Engineering of the National Technical University of Athens, Greece.
Data sharing is increasingly important. Companies share data internally across business units to gain business insights, they share data externally with data analytics vendors, and they often share data simply to make money. Ensuring the anonymity of users in the data set is necessary. The process of approving or certifying anonymization however is costly, time consuming, and uncertain. Current approaches to anonymization are ad hoc at best. They require a custom strategy for each new data sharing scenario, and it is often unclear whether the data is really anonymized or not.
In this informative and lively session, corporate DPOs, vendors of analytics solutions, and privacy researchers share their experiences with data anonymization and the approval process. They provide case studies illustrating the pitfalls of "do it yourself" anonymization, and show how some new ready-for-use anonymization can eliminate the delays and guesswork of data anonymization.
The workshop will be held May 25 in San Jose, CA.
For over 40 years, the holy grail of database anonymization is a system that allows a wide variety of statistical queries with minimal answer distortion, places no limits on the number of queries, is easy to configure, and gives strong protection of individual user data. This keynote presents Diffix, a database anonymization system that promises to finally bring us within reach of that goal. Diffix adds noise to query responses, but "fixes" the noise to the response so that repeated instances of the same response produce the same noise. While this addresses the problem of averaging attacks, it opens the system to "difference attacks" which can reveal individual user data merely through the fact that two responses differ. Diffix proactively examines queries and responses to defend against difference attacks. This talk presents the design of Diffix, gives a demo of a commercial-quality implementation, and discusses shortcomings and next steps.
The 26th International World Wide Web Conference (WWW) took place in Perth (Australia) in April 2017.
Our understanding of exploit documents as a vector to deliver targeted malware is limited to a handful of studies done in collaboration with the Tibetans, Uyghurs, and political dissidents in the Middle East. In this measurement study, we present a complementary methodology relying only on publicly available data to capture and analyze targeted attacks with both greater scale and depth. In particular, we detect exploit documents uploaded over one year to a large anti-virus aggregator (VirusTotal) and then mine the social engineering information they embed to infer their likely targets and contextual information of the attacks. We identify attacks against two ethnic groups (Tibet and Uyghur) as well as 12 countries spanning America, Asia, and Europe. We then analyze the exploit documents dynamically in sandboxes to correlate and compare the exploited vulnerabilities and malware families targeting different groups. Finally, we use machine learning to infer the role of the uploaders of these documents to VirusTotal (i.e., attacker, targeted victim, or third-party), which enables their classification based only on their metadata, without any dynamic analysis. We make our datasets available to the academic community.
- Fairness Beyond Disparate Treatment & Disparate Impact: Learning Classification without Disparate Mistreatment
- Modeling the Dynamics of Online Learning Activity
- Distilling Information Reliability and Source Trustworthiness from Digital Traces
- Optimizing the Recency-Relevancy Trade-off in Online News Recommendations
- Predicting the Success of Online Petitions Leveraging Multi-dimensional Time-Series
The 26th International World Wide Web Conference (WWW) will take place in Perth, Australia in April 2017.
To receive full consideration, applications should be received by December 15, 2016. For further details see our job ad.
EMSOFT brings together researchers and developers from academia, industry, and government to advance the science, engineering, and technology of embedded software development. Since 2001, EMSOFT has been the premier venue for cutting-edge research in the design and analysis of software that interacts with physical processes, with a long-standing tradition for results on cyber-physical systems, which compose computation, networking, and physical dynamics. See the ESWEEK homepage for further details.
- A promising semantics for relaxed-memory concurrency
- Relational cost analysis
- Thread modularity at many levels: a pearl in compositional verification
- RedQueen: An Online Algorithm for Smart Broadcasting in Social Networks
- Uncovering the Dynamics of Crowdlearning and the Value of Knowledge
CAV 2017 is the 29th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis and synthesis methods for hardware and software systems. The CAV home page has more information.
- Quantifying the Effect of Period Ratios on Schedulability of Rate Monotonic
- On the Problem of Finding Optimal Harmonic Periods
RTNS 2016 will be held from October 19 to October 21 in Brest, France.
- A Blocking Bound for Nested FIFO Spin Locks
- Global Scheduling Not Required: Simple, Near-Optimal Multiprocessor Real-Time Scheduling with Semi-Partitioned Reservations
The European Research Council (ERC) is a pan-European funding body that supports cutting-edge research. It offers funding for groundbreaking research projects of the highest scientific quality across Europe, across all research areas. Talented researchers from all over the world can receive funding for excellent research in Europe. The ERC Consolidator Grant offers funding for researchers with 7 to 12 years of experience after achieving a PhD.
The RustBelt Project
A longstanding question in the design of programming languages is how to balance safety and control. C-like languages give programmers low-level control over resource management at the expense of safety, whereas Java-like languages give programmers safe high-level abstractions at the expense of control.
Rust is a new language developed at Mozilla Research that marries together the low-level flexibility of modern C++ with a strong "ownership-based" type system guaranteeing type safety, memory safety, and data race freedom. As such, Rust has the potential to revolutionize systems programming, making it possible to build software systems that are safe by construction, without having to give up low-level control over performance.
Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold. To rule out data races and other common programming errors, Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art.
In this project, we aim to equip Rust programmers with the first formal tools for verifying safe encapsulation of "unsafe" code. Any realistic languages targeting this domain in the future will encounter the same problem, so we expect our results to have lasting impact. To achieve this goal, we will build on recent breakthrough developments by the PI and collaborators in concurrent program logics and semantic models of type systems.
In 2015, Joel was awarded an ERC Consolidator Grant, which provides almost 2 million euros of research funding over a period of five years. He is also the recipient of the 2010 Roger Needham Award, given annually "for a distinguished research contribution in Computer Science by a UK-based researcher within ten years of his or her PhD."
Joel will join MPI-SWS from the University of Oxford, where he is a Professor of Computer Science and Fellow of St John's College. Joel holds a BSc and MSc in Mathematics from McGill University, and received his PhD in Computer Science from Oxford in 2001. He subsequently did postdoctoral work at Tulane University and Carnegie Mellon University.
The Heidelberg Laureate Forum gives young computer science and math researchers the opportunity to interact with some of the world's top scientists. The speakers for the 2014 Forum, for example, include 14 different Turing Award winners, as well as numerous winners of the Fields Medal and the Abel Prize.
Majumdar won the award for his 2004 paper, Abstractions From Proofs, which was coauthored with Thomas Henzinger, Ranjit Jhala, and Kenneth McMillan. The paper introduced a technique to automatically find program abstractions using logical interpolation and showed the effectiveness of the technique in software verification.
Over the next six years their project "imPACT: Privacy, Accountability, Compliance, and Trust in Tomorrow's Internet" will receive almost 10 million euros, which will allow them to explore how to protect users against eavesdropping and fraud on the Internet without restricting trade, freedom of expression or access to information.
Brandenburg's dissertation, "Scheduling and Locking in Multiprocessor Real-Time Operating Systems," was also selected for the 2012 Linda Dykstra Distinguished Dissertation Award, which recognizes the best dissertation among all graduates in the fields of mathematics, physical sciences, and engineering at the University of North Carolina at Chapel Hill.
Allen Clement obtained his Ph.D. at the University of Texas at Austin in 2011. Allen's research aims at designing and building systems that continue to work despite the myriad of things that go 'wrong' in deployed systems, including broken components, malicious adversaries, and benign race conditions. His research builds on techniques from distributed systems, security, fault tolerance, and game theory.
Cristian Danescu-Niculescu-Mizil is joining us from Cornell University, where he obtained his PhD in computer science. Cristian's research aims at developing computational frameworks that can lead to a better understanding of human social behavior, by unlocking the unprecedented potential of the large amounts of natural language data generated online. His work tackles problems related to conversational behavior, opinion mining, computational semantics and computational advertising.
Rupak Majumdar and Zhenyue Long, along with Georgei Calin and Roland Meyer at TuKL, have received the ETAPS 2012 best paper award for their paper "Language-Theoretic Abstraction Refinement".
Rupak Majumdar has also received (along with Jason Cong, Bin Liu, and Zhiru Zhang) the 2012 ACM TODAES Best Paper Award for his 2010 TODAES article "Behavior-Level Observability Analysis for Operation Gating in Low-Power Behavioral Synthesis".
A recent WWW 2012 paper by Krishna Gummadi, Bimal Viswanath, and their coauthors was covered by GigaOM, a popular technology news blog, in an article titled Who's to blame for Twitter spam? Obama, Gaga, and you.
Steven le Blond's work on security flaws in Skype and other peer-to-peer applications has been receiving global media attention: WSJ, Le Monde (French), die Zeit (German), Daily Mail, New Scientist, Slashdot, Wired, and the New Scientist "One Percent" blog.
The ACM SIGPLAN Most Influential PLDI Paper Award is given each year for a paper that is ten years old and has been highly influential in the area of programming languages.
Rupak's 2001 paper, "Automatic Predicate Abstraction of C Programs," was coauthored with Thomas Ball, Todd Millstein, and Sriram Rajamani. The paper presented the predicate abstraction technology underlying the SLAM project. The technology is now part of Microsoft's Static Driver Verifier in the Windows Driver Development Kit. This is one of the earliest examples of automation of software verification on a large scale and the basis for numerous efforts to expand the domains that can be verified.
The ACM SIGCOMM Test of Time Award recognizes papers published 10 to 12 years in the past in Computer Communication Review or any SIGCOMM sponsored or co-sponsored conference that is deemed to be an outstanding paper whose contents are still a vibrant and useful contribution today.
Paul's 2001 paper, "A Scalable Content-Addressable Network," was coauthored with Mark Handley, Richard Karp, Sylvia Ratnasamy, and Scott Shenker. This paper is one of four highly influential papers that laid the foundation for P2P systems based on distributed hash tables (DHTs).
We are pleased to announce that three new faculty will join MPI-SWS this fall.
Björn Brandenburg is joining us from the University of North Carolina at Chapel Hill (UNC), where he obtained his Ph.D. in computer science. Björn's research interests include multiprocessor real-time system, real-time synchronization protocols, and operating systems. Björn is the lead designer and developer of LITMUSRT, an extension of the Linux kernel for real-time scheduling and synchronization on multicore platforms.
Deepak Garg is joining us from the Cybersecurity Lab (CyLab) at Carnegie Mellon University, where he was a post-doctoral researcher. He obtained his Ph.D. from Carnegie Mellon's Computer Science Department. His research interests are in the areas of computer security and privacy, formal logic and programming languages. He is specifically interested in logic-based models of secure systems and formal analysis of security properties of systems.
Ruzica Piskac is joining us from EPFL, where she has completed her Ph.D. in computer science. The goal of her research is to make software development easier and software more reliable via automated reasoning techniques. She is specifically interested in decision procedures, their combinations and applications in program verification and software synthesis.
Andreas Haeberlen, now an Assistant Professor in the department of Computer and Information Science at the University of Pennsylvania, has received the award for his proposal "Evidence in Federated Distributed Systems."
Alan Mislove, now an Assistant Professor in the College of Computer and Information Science at Northeastern University, has received the award for his proposal "Systems for the Emerging Patterns of Content Exchange."
The Humboldt Research Award is granted "in recognition of a researcher's entire achievements to date to academics whose fundamental discoveries, new theories, or insights have had a significant impact on their own discipline and who are expected to continue producing cutting-edge achievements in the future."
The study, which will be presented at the ACM Internet Measurement Conference (IMC) in November, looks at the targeting behavior of Google and Facebook. While the goal of the study was to understand targeting in general, the researchers discovered that gay Facebook users can unknowingly reveal to advertisers that they are gay simply by clicking on an ad targeted to gay men. The ads appear innocuous in that they make no mention of targeting gay users (for instance, an ad for a nursing degree). A user's sexual orientation can be leaked even if the user made his sexual orientation private using Facebook's privacy settings.
This study was done as part of a broader research project to design techniques for making advertising more private.
Viktor's research contributions include inventing new concurrent program logics (RGSep & deny/guarantee); developing automated verification tools (SmallfootRG & Cave) for proving correctness properties of concurrent algorithms; and verifying some particularly challenging algorithms manually (e.g., mcas), mechanically (e.g., fast congruence closure), or automatically (e.g., lazy set).
Viktor received his B.A. degree in Computer Science in 2004 and his Ph.D. degree in Computer Science in 2008 both from the University of Cambridge. After that, he held post-doctoral research positions at Microsoft Research and at the University of Cambridge.
Rupak's research spans the spectrum of formal verification techniques, ranging from theoretical foundations of logic and automata theory to practical software engineering tools that systematically analyze thousands of lines of code for programmer errors. In the field of software model checking, Rupak has made major contributions. Rupak, along with Ranjit Jhala, wrote the the model checker Blast, which is able to analyze over 100,000 lines of code for complex temporal properties. This achievement was a major milestone and proof of feasibility in the field of software verification and led to a flurry of academic and industrial activity in the area.
Rupak joins MPI-SWS from the University of California, Los Angeles, where he was on the faculty of the computer science department. Prior to that, Rupak received his Ph.D. degree in Computer Science from the University of California at Berkeley, and his B.Tech. degree in Computer Science from the Indian Institute of Technology at Kanpur.
The external scientific member appointment is a courtesy appointment, which acknowledges the member's scientific excellence, as well as his or her close collaboration and contribution to joint research projects with MPI-SWS faculty and researchers.
Robert Harper has been a professor in the Computer Science Department at Carnegie Mellon University since 1988. He received his Ph.D. in Computer Science from Cornell University in 1985, and was a post-doctoral research fellow at the Laboratory for Foundations of Computer Science at Edinburgh University from 1985-1988. He is best known for his work on the design, definition, and implementation of Standard ML; the design and application of the LF logical framework; the type-theoretic foundations of modularity in programming languages; the use of typed intermediate languages for certified compilation; the co-invention of self-adjusting computation for dynamic algorithms; and the application of fundamental theory to practical software systems. His current interests include mechanization of the metatheory of programming languages, the integration of types and verification, and the application of programming language theory to computer security.
Founded in 1948, the Max Planck Society is a non-profit scientific organization affiliated with the Max Planck Institutes. The Society awards the Otto Hahn Medal annually to young scientists in recognition of outstanding scientific achievement. In addition to a stipend, the award gives winners preference for grants enabling them to conduct research abroad for one year.
Alan Mislove, Bimal Viswanath, Krishna P. Gummadi, and Peter Druschel's work on inferring user profiles in online social networks has received media coverage from Slashdot.
Such systems abound in many areas of computer science. For example, physical simulations often involve objects that move continuously over time, databases host and process data that changes over time (e.g., by introduction of new information records), and connectivity in networks and distributed systems changes as links go down or come alive.
Umut's primary research focus has been self-adjusting computation, where computations respond automatically to modifications to their data. With his collaborators, he designs languages for developing self-adjusting programs, researches techniques for analyzing their complexity, and evaluates the proposed techniques by considering problem domains such as computational geometry, machine learning, and scientific computing. Umut's other interests include parallel computing, databases, and design and implementation of high-level languages.
Umut Acar received his B.S. in Computer Science from Bilkent University-Turkey in 1997, his M.A. from University of Texas at Austin in 1999, and his Ph.D. from Carnegie Mellon University in 2004. Umut joins MPI-SWS from the Toyota Technological Institute of Chicago, where he was an assistant professor from 2005 to 2009.
The EAPLS award goes to the best contribution in the area of programming languages among CC, ESOP, and TACAS—three member conferences of ETAPS, the European Joint Conferences on Theory and Practice of Software.
The award-winning paper describes the design and implementation of an automatic invariant generator that can be used in the verification of imperative programs. The authors' new approach makes constraint solving—and hence invariant generation—more scalable by adding information obtained from static abstract interpretation as well as dynamic execution of the program.
ETAPS, established in 1998, is a confederation of five annual conferences, accompanied by satellite workshops and other events. It is a primary forum for academic and industrial researchers working on topics relating to Software Science. Previous EAPLS best paper award winners are listed at http://www.eapls.org/pages/topic_05_awards/.