Jan Vitek

My research focus on design and implementation of programming abstractions in areas that have included real-time embedded systems, concurrent and distributed systems and more recently scalable data analytics.

I have published in venues that specialize in Programming Languages, Virtual Machines, Compilers, Software Engineering, Real-time Computing, and Bioinformatics.

I enjoy beautiful code that solves real-world problems.

Software & papers should be free. Open access

Research should be repeatable and replicated. The real software crisis


Czech by birth.
Swiss by adoption, I miss the Alps.

Jan Vitek is a Professor of Computer Science at Northeastern University. He holds degrees from the University of Geneva (PhD'99, BS'89) and University of Victoria (MS'95). Professor Vitek works on topics related to the design and implementation of programming languages. In the Ovm project, he led the implementation of the first real-time Java virtual machine to be successfully flight-tested. Together with Noble and Potter, he proposed a concept that became known as Ownership Types. Prof Vitek was one of the designers of the Thorn language. He works on gaining a better understanding of the JavaScript language and is now looking at supporting scalable data analysis in R. Prof Vitek chaired ACM SIGPLAN; he is the Chief Scientist at Fiji Systems, he is a vice chair of AITO; was a vice chair of IFIP WG 2.4. He chaired PLDI, ISMM and LCTES and was program chair of ESOP, ECOOP, VEE, Coordination, and TOOLS. Vitek has started a number of successful workshop series, including MOS on Mobile Objects, IWACO, STOP, and TRANSACT. He is/was on the steering committees of ECOOP, JTRES, TRANSACT, ICFP, OOPSLA, POPL, PLDI and LCTES.

Jan Vitek

Professor of Computer Science

College of Computer &
Information Science
Northeastern University
440 Huntington Ave,
Boston, MA 02115

Skype: vitek_jan
Email: j.vitek@neu.edu
Office: Yes
H-index: 45
DBLP: Here
Ln: Here
FB: Here
Lab: PRL


I am co-oganizing the first Programming Language Implementation Summer School, in May 2017 in Italy.
Our work on analysis of JavaScript will be supported by a 2016 Google Faculty Research Award
I am co-oganizing the second Curry On, a mixer to get academia to meet the real world, July in Rome! Curry On
Build a JIT with LLVM was a class at CVUT taught with Oli Fluckiger and Petr Maj [source]
I'm ECOOP's Comfy Chair and Summer School Czar, it is happening July 5-10 in Prague ECOOP
I have become past Chair of SIGPLAN, here is my final report.
Heather Miller and I oganized the first Curry On, a mixer to get academia to meet the real world, July 6-7 in Prague Curry On
Adam Welc and I are running the RIOT workshop on tools and implementation techniques for the R language, July 5th in Prague
Prasad Kulkarni and I have created the ML4PL workshop on machine learning meets programming languages, July 6th in Prague
ECOOP goes Open Access with LIPIcs–Leibniz International Proceedings in Informatics. Both authors and AITO (Exec & members) were in favor. Open access
A paper with Shriram Krishnamurthi arguing for artifact evaluation is in now CACM. The real software crisis
Our work on implemnentations of the R language will be supported by a 2015 Google Faculty Research Award



SPLASH'18 General Chair
ECOOP'15 Comfy Chair
ESOP'15 Program Chair
POPL'15 Artiface Evaluation Chair
PLDI'14 Artiface Evaluation Chair
ECOOP'13 Artiface Evaluation Chair
PLDI'12 General Chair
LCTES'11 General Chair
ISMM'10 General Chair
TOOLS'10 Program Chair
JTRES'10 Program Chair
ECOOP'08 Program Chair
COORD'07 Program Chair
TRANSACT'06 General Chair
VEE'05 Program Chair
PLDI'05 Tutorial Chair

Event Organizer

PLISS Programming Lanugage Implementation Summer School, 2017
ESS ECOOP Summer School: 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017
REMC'16 Dagstuhl Seminar 16111 on Rethinking Experimental Methods in Computing
SPLASH-I SPLASH-I track: 2013, 2015
SOTU.JS'14 Stat of the Union: JavaScript
DALI'13 NSF Workshop on Dynamic Languages for Scalable Data Analytics
PDB'13 NSF Workshop on Programming with Big Data
VEESC'10 Workshop on Dynamic Languages for Scientific Computing
TiC Trends in Concurrency: 2006, 2008, 2010
TMW'10 NSF Transactional Memory Workshop
WG2.4 IFIP WG2.4 meeting in Bormio
TfT'05 Dagstuhl Workshop on Types for Tools


Bioconductor Member, Scientific Advisory Board, 2017--
SIGPLAN Past Chair, 2015--2018
SIGPLAN Chair, 2012--2015
AITO Vice President, 2010--Now
IFIP WG2.4 Vice Chair, 2011--2015
Comin Labs Member, Advisory Board, 2011--2016
JSR-302 Member, Expert Group, 2008--2013
LCTES Member, SC, 2011--2015
ICFP Member, SC, 2012--2015
OOPSLA Member, SC, 2012--2015
PLDI Member SC, 2012--2018; Chair SC, 2014--2016
POPL Member, SC, 2012--2015
ISMM Member, SC, 2010--2015
JTRES Member, SC, 2010--2017
TRANSACT Founding Member, SC, 2006--2017
RIOT Founding Member, SC, 2015--Now
ML4PL Founding Member, SC, 2015
STOP Founding Member, SC, 2011--Now
JOT Editor in Chief, 2013--2014


2013 Purdue Undergraduate Advising Award
2011 Purdue University Faculty Scholar
2011 Purdue Undergraduate Advising Award
2011 Microsoft SEIF Research Award
2006 IBM Faculty Award
2001 NSF CAREER Award

Invited Talks

FedCSIS'17 Data Analysis for the Masses. Prague
Scala'16 This Is Not A Type: Gradual Typing in Practice. Amsterdam
PLMW'16 My twenty five years in OO. Amsterdam
MLOC.JS'15 Benchmarks killed the beast: Understanding JS performance for fun and profit. International Large Scale JavaScript Conference, Budapest
PLMW'15 Repeatability, reproducibility and rigor in CS research. Programming Language Mentoring Workshop, Mumbai
VEE'14 The Case for the Three Rs of Systems Research: Repeatability, Reproducibility and Rigor
SCR'13 JavaScript Programmers Hate You: An ode to dynamic languages. Workshop on Software Correctness and Reliability, Zurich PDF Video
PLMW'13 Planet Dynamic or: How I Learned to Stop Worrying and Love Reflection. SIGPLAN Programming Languages Mentoring Workshop, Rome
FTFJP'13 JavaScript Programmers Hate You. Formal Techniques for Java-like Programs, Montpellier
APLAS'12 Planet Dynamic or: How I Learned to Stop Worrying and Love Reflection. Asian Symposium on Programming Languages and Systems, Kyoto
Aki'12 Thorn: Objects, Scripts and more... Concurrent Objects and Beyond Symposium in Honor of Professor Akinori Yonezawa’s 65th Birthday, Kobe
MSR'11 The Rise of Dynamic Languages for Scientific Computing, MSR Faculty Summit Video
MVD 10 Is Java Ready for Real-time? PDF
APLWA'10 Of Scripts and Programs Tall tales, Urban Legends and Future Prospects PDF
DLS'09 Of Scripts and Programs Tall tales, Urban Legends and Future Prospects PDF
TOOLS'09 Programming models for Real-time and Concurrency. PDF
FCS'05 Language-based Intrusion Detection, Foundations of Computer Security
FOSAD'04 Coordination and Security, School on Foundations of Security Analysis and Design PDF

Program Committees

APLAS Asian Symp. on Programming Languages and Systems, 2014
ARRAY Workshop on Libraries, Languages, and Compilers for Array Programming, 2014, 2015, 2017
AIOOL Workshop on Abstract Interpretation of Object-oriented Languages, 2005
ACP4IS Workshop on Aspects, Components, and Patterns for Infrastructure Software, 2003, 2004
ASA/MA Agent Systems and Applications/ Mobile Agents, 2001
AISB Symposium on Software mobility and adaptive behaviour, 2001
Bytecode Workshop on Bytecode Semantics, Verification, Analysis and Transformation, 2007, 2008
CC Conference on Compiler Construction, 2003, 2008, 2012, 2014
CSF Computer Security Foundations Symposium, 2008
CORDIE Workshop on Concurrency, Real-Time and Distribution in Eiffel, 2006
COORD Conference on Coordination Models and Languages, 2005, 2009
CPS Workshop on Cyber-Physical Systems, 2008, 2009
CD Component Deployment, 2002, 2004
CSJP Workshop on Concurrency and Synchronization in Java Programs, 2004
DATE DATE Conference, Model Based Design of Embedded Systems track, 2010
DLS Dynamic Language Symposium Conference, 2010, 2014, 2015, 2016, 2017
DOSW Distributed Object Security Workshop, 1999
ECOOP European Conference on Object-Oriented Programming, 1998, 2000, 2001, 2002, 2003, 2007, 2008, 2009, 2010, 2013, 2017
ESOP European Symposium on Programming, 2002, 2007, 2009, 2011, 2015, 2016.
EMSOFT Conference on Embedded Software, 2011.
EUC Conference on Embedded and Ubiquitous Computing, 2009, 2010
FEAST Workshop on Forming an Ecosystem Around Software Transformation, 2017


FOCLASA Foundations of Coordination Languages and Software Architectures, 2007
FOOL Foundations of Object-Oriented Languages, 2013
GCM Workshop on Green Computing Middleware, 2011.
GPCE Generative Programming: Concepts & Experiences, 2013
MASS Symposium on Multi-Agent Security and Survivability, 2004
FTfJP Workshop on Formal Techniques for Java-like Programs, 2005
HCSP Workshop on High Confidence Software Platforms for Cyber-Physical Systems, 2006
HotPar Topics in Parallelism, 2013
ICOOOLPS Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems, 2006, 2013, 2015, 2017
ICALP International Conference on Automata, Languages and Programming, 2000
ICFP International Functional Programming Conference, 2005
ISORC International Symposium on Object and componentoriented Real-time Computing, 2012.
IWMSE International Workshop on Multicore Software Engineering, 2010
IWACO International Workshop on Aliasing, Confinement and Ownership, 2003, 2007, 2014
IWAOOS Intercontinental Workshop on Aliasing in Object- Oriented Systems, 1999
JTRes Workshop on Java Technologies for Real-Time and Embedded Systems, 2008, 2007, 2006, 2005, 2004, 2003, 2008, 2009, 2010
JFLA Journees Francophones des Langages Applicatifs, 2000, 1998, 1995
ManLang International Conference on Managed Languages and Runtimes, 2017
MOS Mobile Objects Systems Workshop, 2004, 2003, 2002, 2001, 2000, 1999, 1998, 1997, 1996, 1995
MUSEPAT Multicore Software Engineering, Performance, Applications, and Tools, 2016
PLACES Programming Language Approaches to Concurrency and Communication-cEntric Software, 2009, 2010, 2011, 2012
PLAS Workshop on Programming Languages and Analysis for Security, 2007
PLASTIC Workshop on Programming Language And Systems Technologies for Internet Clients, 2011
PLDI Programming Language Design and Implementation, 2002, 2010, 2013
PODC Symposium on Principles of Distributed Computing, 2010
POPL Principles of Programming Languages, 2001, 2008, 2011.
PPPJ conference on Principles and Practice of Programming in Java, 2006
RTAS Real-Time and Embedded Technology and Applications Symposium, 2011.
RTSS Real-Time System Symposium, 2009, 2010, 2011.
SACMAT Symposium on Access Control Models and Technologies, 2001
SANCS Workshop on Software Architectures for Next-generation Cyber-physical Systems, 2015
SCALA Scala Symposium, 2015
STOP Script to Program Evolution Workshop, 2016
OBT Off-the Beaten Track, 2014
OOPS Object Oriented Programming Languages and Systems 2005, 2004
OOPSLA Object-Oriented Programming Systems, Languages, and Applications, 2000, 2004, 2007, 2008, 2016
SecCo Workshop on Security Issues in Concurrency, 2003, 2004, 2007
TRUST Workshop on Reproducible Research Methodologies and New Publication Models, 2014
RIOT R Implementation Optimization and Tooling Workshop, 2015, 2016, 2017
RUMPLE Workshop on ReUsable and Modular Programming Language Ecosystems, 2016
VEE Conference on Virtual Execution Environments, 2011
VMIL Workshop on Virtual Machines and Intermediate Languages, 2009
WASDeTT Workshop on Academic Software Development Tools and Techniques, 2013
WWW The Web Conference, 2018



Dynjs Analyze the dynamic behavior of JavaScript programs and its implications on analyses and security. Code available for JSBench and JSLocker. Data available for our analysis papers.
Fiji The Fiji real-time JVM and Fiji C1 compiler run on on a broad range of HW/OS (ARM, PowerPC and x86, RTEMS, Linux, Darwin), with deterministic garbage collection, or safe GC-less allocation. Allow to create mixed-criticality systems with isolation and partitioning.
AllR Tools related to the R programming language including the Purdue implementation of the FastR virtual machine (2014), timeR, testR and benchR. Code and data available. FastR has been transitionned to Oracle.


AJ Data-centric concurrency control for Java using atomic-sets. Project completed in 2013 in collaboration with IBM research. Data available.
FlexoTasks Very low latency real-time streaming in Java. Project completed in 2010 in collaboration with IBM research. Code and data available.
Thorn Thorn is a dynamically-typed concurrent language in which lightweight isolated processes communicate by message passing. Thorn includes aggregate data types, class-based objects, first-class functions, modules, and features for gradual evolution of scripts to programs. Completed in 2010.
Ovm The Ovm project aims to develop a customizable framework for research in virtual machines and object-oriented programming language runtime systems. Completed in 2009. Code available.
oSCJ An open-source implementation of a subset of Safety-Critical Java. Completed in 2010. Code available.
CDx CDx is an open source application benchmark suite that targets hard and soft real-time Java virtual machines. Completed in 2009. Code and data available.
Prismj Real-time Java controls for a ScanEagle UAV. Winner of DUKE's Choice award. Completed in 2005.
stmbench7 A benchmark for evaluating software transactional memory implementations. The benchmark aims at providing a workload that is both realistic and non-trivial to scale. Code available. Completed in 2007.
MBA MBA is a Java program for automated assignment and assessment of uncertainty of protein backbone NMR. Completed in 2006. Code and data available.


  • OOSPLA'17Déj Vu: A Map of Code Duplicates on GitHub

    Authors: Crista Lopes, Petr Maj, Jan Vitek

    Abstract: Previous studies have shown that there is a non-trivial amount of duplication in source code. This paper analyzes a corpus of 2.6 million non-fork projects hosted on github representing over 258 million files written in Java, C++, Python, and JavaScript. We found that this corpus has a mere 54 million unique files. In other words, 79% of the code on github consists of clones of previously created files. There is considerable variation between language ecosystems. JavaScript has the highest rate of file duplication, only 7% of the files are distinct. Java, on the other hand, has the least duplication, 65% of files are distinct. Focusing on files that have some differences, we found between 31% and 43% of files with strong similarities. Lastly, we made a project-level analysis, and found that between 10% and 20% of the projects contain at least 80% of files that can be found elsewhere. These surprisingly high rates of duplication have implications for systems built on open source software as well as for researchers interested in analyzing large code bases. As a concrete artifact of this study, we have created Dejavu, a publicly available map of code duplicates in github repositories. .

    Venue: PACM PL (OOPSLA)

  • OOSPLA'17 Orca: Leveraging Types and Messaging for Fully Concurrent GC

    Authors: Sylvain Clebsch, Juliana Franco, Sophia Drossopoulou, Albert Mingkun Yang, Tobias Wrigstad, Jan Vitek

    Abstract: Orca is a concurrent and parallel garbage collector for actor programs, which does not require any stop-the- world steps, or synchronisation mechanisms, and which has been designed to support zero-copy message passing and sharing of mutable data. Orca is part of the runtime of the actor-based language Pony. Pony’s runtime was co-designed with the Pony language. This co-design allowed to exploit certain language properties in order to optimise performance of garbage collection. Namely, Orca relies on the absence of race conditions in order to avoid read/write barriers, and it leverages the actor message passing for synchronisation among actors. This paper describes Pony, its type system, and the Orca garbage collection algorithm. An evaluation of the performance of Orca suggests that is fast and scalable for idiomatic workloads.

    Venue: PACM PL (OOPSLA)

  • ECOOP'17Parallelizing Julia with a Non-invasive DSL

    Authors: Todd Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman

    Abstract: Computational scientists often prototype software using productivity languages that offer high-level programming abstractions. When higher performance is needed, they are obliged to rewrite their code in a lower-level efficiency language. Different solutions have been proposed to address this tradeoff between productivity and efficiency. One promising approach is to create embedded domain-specific languages that sacrifice generality for productivity and performance, but practical experience with DSLs points to some road blocks preventing widespread adoption. This paper proposes a non-invasive domain-specific language that makes as few visible changes to the host programming model as possible. We present ParallelAccelerator, a library and compiler for high-level, high-performance scientific computing in Julia. ParallelAccelerator’s programming model is aligned with existing Julia programming idioms. Our compiler exposes the implicit parallelism in high-level array-style programs and compiles them to fast, parallel native code. Programs can also run in “library-only” mode, letting users benefit from the full Julia environment and libraries. Our results show encouraging performance improvements with very few changes to source code required. In particular, few to no additional type annotations are necessary.

    Venue: European Confence on Object-Oriented Programming (ECOOP)

    DOI: 10.4230/LIPIcs.ECOOP.2017.4

    Artifact: 10.4230/DARTS.3.2.7

  • ITP'17 Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology

    Authors: Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

    Abstract: Concurrent garbage collection algorithms are a challenge in the area of concurrent program verification. We proposed a mechanized proof methodology based on the popular Rely-Guarantee (RG) proof technique. We design a specific compiler intermediate representation (IR) with strong type guarantees, dedicated support for abstract concurrent data structures, and high-level iterators on runtime internals. In addition, we define an RG program logic supporting an incremental proof methodology where annotations and invariants can be progressively enriched. We formalize the IR, the proof system, and prove the soundness of the methodol- ogy in the Coq proof assistant. Equipped with this IR, we prove a fully concurrent garbage collector where mutators never have to wait for the collector.

    Venue: International Conference on Interactive Theorem Proving (ITP)


  • RTAS'17Making Android Run on Time
    Authors: Yin Yan, Karthik Dantu, Steven Y. Ko, Jan Vitek, Lukasz Ziarek
    Abstract: Time predictability is difficult to achieve in the complex, layered execution environments that are common in modern embedded devices. We consider the possibility of adopting the Android programming model for a range of embedded applications that extends beyond mobile devices, under the constraint that changes to widely used libraries should be minimized. The challenges we explore include: the interplay between real-time activities and the rest of the system, how to express the timeliness requirements of components, and how well those requirements can be met on stock embedded platforms. We report on the design and implementation of an Android virtual machine with soft-real-time support, and provides experimental data validating feasibility over three case studies. Venue: Real-time and Embedded Technology and Application Symposium (RTAS)
    DOI: 10.1109/ICTAS.2017.7920653
  • POPL'16Is Sound Gradual Typing Dead?
    Authors: Asumu Takikawa, Dan Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen
    Abstract: Programmers have come to embrace dynamically-typed languages for prototyping and delivering large and complex systems. When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. In response, researchers have explored the idea of gradually-typed programming languages which allow the incremental addition of type annotations to software written in one of these untyped languages. Some of these new, hybrid languages insert run-time checks at the boundary between typed and untyped code to establish type soundness for the overall system. With sound gradual typing, programmers can rely on the language implementation to provide meaningful error messages when type invariants are violated. While most research on sound gradual typing remains theoretical, the few emerging implementations suffer from performance overheads due to these checks. None of the publications on this topic comes with a comprehensive performance evaluation. Worse, a few report disastrous numbers. In response, this paper proposes a method for evaluating the performance of gradually-typed programming languages. The method hinges on exploring the space of partial conversions from untyped to typed. For each benchmark, the performance of the different versions is reported in a synthetic metric that associates runtime overhead to conversion effort. The paper reports on the results of applying the method to Typed Racket, a mature implementation of sound gradual typing, using a suite of real-world programs of various sizes and complexities. Based on these results the paper con- cludes that, given the current state of implementation technologies, sound gradual typing faces significant challenges. Conversely, it raises the question of how implementations could reduce the overheads associated with soundness and how tools could be used to steer programmers clear from pathological cases.
    Venue: Principles of Programming Languages (POPL)
    DOI: 10.1145/2914770.2837630
    Artifact: http://www.ccs.neu.edu/home/asumu/artifacts/popl-2016/
  • ECOOP'15Concrete Types for TypeScript
    Authors: Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek
    Abstract: TypeScript extends JavaScript with optional type annotations that are, by design, unsound and, that the TypeScript compiler discards as it emits code. This design point preserves programming idioms developers are familiar with, and allows them to leave their legacy code unchanged, while offering a measure of static error checking in annotated parts of the program. We present an alternative design for TypeScript that supports the same degree of dynamism but that also allows types to be strengthened to provide correctness guarantees. We report on an implementation, called StrongScript, that improves runtime performance of typed programs when run on a modified version of the V8 JavaScript engine.
    Venue: European Conference on Object Oriented Programming (ECOOP)
    DOI: 10.4230/LIPIcs.ECOOP.2015.999
    Artifact: http://plg.uwaterloo.ca/~dynjs/strongscript
  • ECOOP'15Cooking the Books: Formalizing JMM Implementation Recipes
    Authors: Gustavo Petri, Jan Vitek and Suresh Jagannathan
    Abstract: The Java Memory Model (JMM) is intended to characterize the meaning of concurrent Java programs. Because of the model's complexity, however, its definition cannot be easily transplanted within an optimizing Java compiler, even though an important rationale for its design was to ensure Java compiler optimizations are not unduly hampered because of the language's concurrency features. In response, the JSR-133 Cookbook for Compiler Writers, an informal guide to realizing the principles underlying the JMM on different (relaxed-memory) platforms was developed. The goal of the cookbook is to give compiler writers a relatively simple, yet reasonably efficient, set of reordering-based recipes that satisfy JMM constraints. We present the first formalization of the cookbook, providing a semantic basis upon which the relationship between the recipes defined by the cookbook and the guarantees enforced by the JMM can be rigorously established. Notably, one artifact of our investigation is that the rules defined by the cookbook for compiling Java onto Power are inconsistent with the requirements of the JMM, a surprising result, and one which justifies our belief in the need for formally provable definitions to reason about sophisticated (and racy) concurrency patterns in Java, and their implementation on modern-day relaxed-memory hardware. Our formalization enables simulation arguments between an architecture-independent intermediate representation of the kind suggested by the Cookbook with machine abstractions for Power and x86. Moreover, we provide fixes for cookbook recipes that are inconsistent with the behaviors admitted by the target platform, and prove the correctness of these repairs.
    Venue: European Conference on Object-Oriented Programming, 2015
    DOI: 10.4230/LIPIcs.ECOOP.2015.999
  • CACM'15The Real Software Crisis: Repeatability as a Core Value
    Authors: Shriram Krishnamurthi, Jan Vitek
    Abstract: Where is the software in programming language research? In our field, software artifacts play a central role: they are the embodiments of our ideas and contributions. Yet when we publish, we are evaluated on our ability to describe informally those artifacts in prose. Often, such prose gives only a partial, and sometimes overly rosy, view of the work. Especially so when the object of discourse is made up of tens of thousands of lines of code that interact in subtle ways with different parts of the software and hardware stack on which it is deployed. Over the years, our community's culture has evolved to value originality above everything else, and our main conferences and journals deny software its rightful place.
    Venue: Communications of the ACM, Vol. 58 No. 3, Pages 34-36
    DOI: 10.1145/2658987
  • TOPLAS'14Atomicity Refinement for Verified Compilation
    Authors: Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek
    Abstract: We consider the verified compilation of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory synchronization and automatic memory management. Our development is framed in the context of the Total Store Order relaxed memory model. Ensuring complier correctness is challenging because high-level actions are translated into sequences of nonatomic actions with compiler-injected snippets of racy code; the behavior of this code depends not only on the actions of other threads but also on out-of-order executions performed by the processor. A naïve proof of correctness would require reasoning over all possible thread interleavings. In this article, we propose a refinement-based proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of low-level concurrent code used to implement managed services. We illustrate our approach with examples taken from the verification of a concurrent garbage collector.
    Venue: ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 36 Issue 2, July 2014, Article No. 6
    DOI: 10.1145/2601339
  • VEE'14A Fast Abstract Syntax Tree Interpteter for R
    Authors: Tomas Kalibera Petr Maj, Floreal Morandat, Jan Vitek
    Abstract:Dynamic languages have been gaining popularity to the point that their performance is starting to matter. The effort required to develop a production-quality, high-performance runtime is, however, staggering and the expertise required to do so is often out of reach of the community maintaining a particular language. Many domain specific languages remain stuck with naive implementations, as they are easy to write and simple to maintain for domain scientists. In this paper, we try to see how far one can push a naive implementation while remaining portable and not requiring expertise in compilers and runtime systems. We choose the R language, a dynamic language used in statistics, as the target of our experiment and adopt the simplest possible implementation strategy, one based on evaluation of abstract syntax trees. We build our interpreter on top of a Java virtual machine and use only facilities available to all Java programmers. We compare our results to other implementations of R.
    Venue: Proceedings of the 10th ACM SIGPLAN/SIGOPS international conference on Virtual execution environments (VEE) Pages 89-102
    DOI: 10.1145/2674025.2576205
  • ISMM'14M3: high-performance memory management from off-the-shelf components
    Authors: David Terei, Alex Aiken, Jan Vitek
    Abstract: Real-world garbage collectors in managed languages are complex. We investigate whether this complexity is really necessary and show that by having a different (but wider) interface between the collector and the developer, we can achieve high performance with off-the-shelf components for real applications. We propose to assemble a memory manager out of multiple, simple collection strategies and to expose the choice of where to use those strategies in the program to the developer. We describe and evaluate an instantiation of our design for C. Our prototype allows developers to choose on a per-type basis whether data should be reference counted or reclaimed by a tracing collector. While neither strategy is optimised, our empirical data shows that we can achieve performance that is competitive with hand-tuned C code for real-world applications.
    Venue: Proceedings of the 2014 international symposium on Memory management (ISMM) Pages 3-13
    DOI: 10.1145/2602988.2602995
Older publication list still to be ported is here.



6240 Parallel Data Processing in MapReduce, F'17, 48 pax
5110 Introduction to Data Science, W'17, 10 pax
6240 Parallel Data Processing in MapReduce, W'15, 48 pax
5010 Program Design Paradigms, F'14, 52 pax


590 Scalable Data Analytics Reading Group, Winter 2014, 12 students.
240 Programming in C, Winter 2014, 240 students.
240 Programming in C, Winter 2012
490 Software for Embedded Systems, Winter 2012
240 Programming in C, Fall 2011
490 Sofware for Embedded Systems, Winter 2011
590 Embedded Computer Systems, Fall 2009
590 Programming Languags Seminar, Fall 2008
590 Programming Languags Seminar, Winter 2008
456 Programming Languages, Winter 2008
456 Programming Languages, Fall 2007
510 Software Engineering, Winter 2006


PhDs Aviral Goel, Celeste Hollenbeck, Petr Maj, Ming-Ho Yee, Benjamin Chung, Olivier Fluckiger, Gregor Richards (2014), Filip Pizlo, Jacques Thomas (2011), Jesper H. Spring (2008 EPFL), Rajeev Gopalakrishna (2006), Bogdan Carbunar (2005), Krzystof Palacz (2004)
MScs Nadya Ortiz (2012), Fadi Meawad (2013), Brandon Hill (2013), Petr Maj (2011), Daniel Tang (2011), Johan Ostlund (2010), Jason Baker (2007), Hiroshi Yamauchi (2007), Christian Grothoff (2005), Andrey Madan (2004), Gergana Markova (2003), Jason M. Fox (2003), James Liang (2002)
BScs Ryan Macnak, Brian Burg (2010), Brett Mravec (2010), Jason Ward (2010), Chris Abernathy (2010), Rob Gevers (2009), Daniel Tang (2008), William Harris (2007), Andrew McClure (2006), Zacchary Wiggins (2005), Paul Kuliniewicz (2004), Wenchang Liu (2004), Filip Pizlo (2004), Chris Willmore (2003), Andrey Madan (2002), Ben Titzer (2003), Adam Lugowski (2002), Josh Moore (200), Gergana Markova (2001), Theodore Witkamp (2003), Javed Siddique (2003) Alen Montz (2004).
PostDocs Konrad Siek (2017--), Filip Krikava (2016--), Paley Li (2015--), Gustavo Petri (2012--2015), Rafal Kolanski (2013-–2014), Michal Malohlava (2012--2013), Floreal Morandat (2011-–2012), Nicholas Kidd (2009-–2010), Christian Hammer (2009-–2011), Ales Plsek (2009-–2011), Sylvain Lebresne (2008-2009), Tomas Kalibera (2007-–2009), Tobias Wrigstad (2007-–2009), Antonio Cunei (2003 – 2008), Jean Privat (2006-–2007), Marek Prochazka (2003-–2005), Jeremy Manson (2003-–2005), Michael Richmond (2002-–2003)


After / Before

Is there any risk of brain damage?

Well, technically speaking, the operation is brain damage, but it's on a par with a night of heavy drinking. Nothing you'll miss.

Eternal Sunshine of the Spotless Mind

Comfy Chair

\'kəm(p)-fē 'cher\
a : a position of authority, state, or dignity
b : he who makes things happen
c : a most feared torture device

With thanks to Camil, Irene and Wilfried.

"I understand radiation better and feel like I could survive an atomic explosion somewhere on the planet, if it wasn't, of course, really close to me."

Amazon.com review of 'All About Radiation' by L. Ron Hubbard.

"DOS computers manufactured by companies such as IBM, Compaq, Tandy, and millions of others are by far the most popular, with about 70 million machines in use worldwide. Macintosh fans, on the other hand, may note that cockroaches are far more numerous than humans, and that numbers alone do not denote a higher life form."

-- New York Times, November 26, 1991.

"Dad, do you say the Pledge of Allegiance at work? ... Ah. Maybe you should, you know... to be a little bit part of this country."

-- Nadia Marie Vitek, Age 8.

Хотели как лучше, а получилось как всегд

-- Viktor Chernomyrdin