Eric Koskinen

Assistant Professor
Stevens Institute of Technology
(201) 216 5071 ยท

I am an Assistant Professor at Stevens Institute of Technology. Previously, I was a Lecturer/Researcher at Yale University and a Visiting Professor at New York University. I received a Ph.D in Computer Science from the University of Cambridge. I also spent time at IBM Watson, Microsoft, and from 2002-2005, I was a Software Engineer at My research yields techniques that improve the way programmers develop reliable and efficient concurrent software for multi-core and distributed systems. To this end, I have made advances along a spectrum of fields, ranging from systems/concurrency methodologies to foundational results in formal methods.

Recent Activities

Continue to: Full List of PublicationFull List of Activities


We are hiring talented PhD students to join us at Stevens! Please contact me if you are interested.

Previous Members

  • Paul Gazzillo, Research Scholar
  • Timos Antonopoulos (Yale)
    Postdoctoral Researcher
  • Brian Zawisza, Undergraduate
  • Ruben Zaccaroni, Undergraduate (NYU)
  • Patrick Yuen, Undergraduate (NYU)


I am currently accepting applications for PhD students in the area of programming languages, formal methods and concurrency. Stevens Computer Science is a rapidly expanding department, with a growing Programming Languages faculty including Eduardo Bonelli, Adriana Compagnoni, Dominic Duggan, Georgios Portokalidis, Eric Koskinen, and David Naumann. We are looking for talented young researchers to join. Successful applicants are expected to participate in a rigorous research program on topics such as programming languages, formal verification, automated reasoning, logic, program analysis, types, concurrency and temporal logic.

We have an active group of students, postdoctoral researchers, and faculty. New students will collaborate with current researchers and students at Stevens, as well as with other faculty members active in the area of programming languages, types, verification, security and systems.

PhD student applicants must have BS degree in Computer Science or a closely related field. An MS degree is not required and students can start in the fall or spring semester. All PhD students are fully funded, including their tuition and a generous stipend. Interested applicants should email me their CV ( and submit an application via



Vertical Composition of Reversible Atomic Objects
T Antonopoulos, P Gazzillo, E Koskinen, Z Shao
Under submission. July 2016.
Games Programs Play: Analyzing Multiplayer Programs
E Koskinen, H Unno, M Vardi
Under submission. July 2016


2018 Dependent Temporal Effects and a Fixpoint Logic for Verification [Slides] NEW
Y Nanjo, H Unno, E Koskinen, T Terauchi.
LICS 2018
Automatic Generation of Precise and Useful Commutativity Conditions NEW
K Bansal, E Koskinen, O Tripp.
TACAS 2018
2017 Adding Concurrency to Smart Contracts NEW
T Dickerson, P Gazzillo, M Herlihy, E Koskinen.
PODC 2017
Proust: A Design Space for Highly-Concurrent Transactional Data Structures
T Dickerson, P Gazzillo, M Herlihy, E Koskinen.
PODC 2017 (Brief Announcement)
Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels NEW
T Antonopoulos, P Gazzillo, M Hicks, E Koskinen, T Terauchi, S Wei
PLDI 2017
Using Abstract Interpretation to Correct Synchronization Faults
P Ferrara, O Tripp, P Liu, E Koskinen
VMCAI 2017
2016 Reducing Crash Recoverability to Reachability [Slides]
E Koskinen, J Yang.
POPL 2016
2015 The Push/Pull model of transactions [Slides] [Technical Report]
E Koskinen, M Parkinson.
PLDI 2015
2014 Local Temporal Reasoning [Full version]
E Koskinen, T Terauchi.
LICS 2014
  Commutativity Race Detection
D Dimitrov, V Raychev, M Vechev, E Koskinen.
PLDI 2014
  Composable Transactional Objects: A Position Paper
M Herlihy (Invited talk), E Koskinen.
ESOP 2014
2013 Turning Nondeterminism into Parallelism
O Tripp, E Koskinen, M Sagiv.
  Reasoning about nondeterminsim in software [slides]
Addendum: A note on support for Strong Until
B Cook, E Koskinen.
PLDI 2013
  Structural Counter Abstraction
K Bansal, E Koskinen, T Wies, D Zufferey.
TACAS 2013
2011 Temporal property verification as a program analysis task [TR] [Slides]
B Cook, E Koskinen, M Vardi.
CAV 2011 Award paper
  Making Prophecies with Decision Predicates [TR] [Slides]
B Cook, E Koskinen.
POPL 2011
2010 Coarse-Grained Transactions [TR] [Slides]
E Koskinen, M Parkinson, M Herlihy.
POPL 2010
2009 Concurrent Non-commutative Boosted Transactions
E Koskinen, M Herlihy.
PODC 2009 (Brief Announcement)
  Control-Flow Refinement and Progress Invariants for Bound Analysis [Slides]
S Gulwani, S Jain, E Koskinen.
PLDI 2009
2008 Dreadlocks: Efficient Deadlock Detection
E Koskinen, M Herlihy.
SPAA 2008
  Checkpoints and Continuations instead of Nested Transactions
E Koskinen, M Herlihy.
SPAA 2008
  Transactional Boosting: A Methodology for Highly-Concurrent Transactional Objects [TR] [Talk]
M Herlihy, E Koskinen.
PPoPP 2008
  BorderPatrol: Isolating Events for Black-box Tracing
E Koskinen, J Jannotti.
EuroSys 2008


Journals, Theses


Automatic Verification of Temporal Alignment (AVTA)

Support from ONR
With Stephen Magill (Galois), Timos Antonopoulos (Yale), Ton-Chanh Le, Cyrus Liu

(Description forthcoming)

Safety/Liveness Verification of Modern Languages

Support from JSPS and NYU Office of the Provost (While at NYU)

Programming languages that use higher-order functionality (e.g. Java, C#, F#, Haskell, Ocaml, Perl, Python, Ruby) have become commonplace. Higher-order language features such as map, grep, Google's Map/Reduce, are used widely and applauded for their simplicity and modularity. While recent techniques have enabled automatic verification of safety/liveness for some industrial software systems, these techniques have been mostly limited to imperative first-order software and cannot be applied to higher-order programming languages.

In an ongoing project, we are demonstrating how one can enrich a language's type system to include temporal logic effects. As we recently showed, these temporal effects can coexist with dependent types to express a wide range of specifications including safety (e.g. method foo(x,f) will not invoke f if x<0), termination (e.g. bar(y) terminates whenever y>0), and mixtures of the two.

• A novel type-and-effect system
• Awarded a grant from NYU Office of the Provost
• Awarded a fellowship from the Japan Society for the Promotion of Science
Paper in LICS 2014
• Implementation in progress
• Background publications including POPL'11, CAV'11, FMSD'12, PLDI'13.

Programming Models for Multicore Concurrency

Support from NSF (1618059 and 1421126)

The recent shift towards concurrent computation has necessitated that we re-think programming. This has lead to a myriad of libraries and language extensions and it is often difficult to understand their respective correctness.

We must enrich our programming languages so that they can incorporate concurrency directly. In this ongoing project, our first objective is to crystalize and formalize effective concurrent programming models. The design goal is for these models to unify existing implementations into a common model.

• Awarded a grant ($250,000) from the NSF
• Synthesizing commutativity conditions (TACAS'18)
• Developed the Push/Pull model of transactions (PLDI'15)
• Developed commutativity race detector (PLDI'14)
• Implementation in progress
• Background publications including POPL'10, PPoPP'08, SPAA'08a, SPAA'08b.

Proving Crash Recoverability

With Junfeng Yang (Columbia), Feng Gou and Drew Malzahn

Software applications run on a variety of platforms (filesystems,virtual slices, mobile hardware, etc.) that do not provide 100% uptime. These applications may crash at any unfortunate moment losing volatile data and, when re-launched, they must be able to correctly recover from potentially inconsistent states left on persistent storage. From a verification perspective, crash recovery bugs can be particularly frustrating because, even when it has been formally proved for a program $P$ that $P \models \varphi$, the proof is foiled by these external events that crash and restart the program.

In this project we are seeking to find formal specifications of crash recoverability, as well as algorithmic verification techniques to automatically prove recoverability.

• Developed a reduction to automaton reachability.
• Proved recoverability of examples from GDBM, LevelDB, LMDB, PostgreSQL, SQLite, VMware and ZooKeeper.
Paper in POPL 2016

Academic Activities

Funding Awards
  • ONR award to study temporal logic-based automatic software verification. June 2017. NEW
  • NSF Award to work on verification of concurrent systems. June 2016.
  • DARPA award to study complexity analysis. December 2014.
  • NSF Award to work on concurrent languages and verification. June 2014.
  • Office of the Provost, New York University. $ 17,000. June 2014.
  • Japan Society for Promotion of Science (JSPS). 1,000,000 JPY. September 2012.
  • Gates Scholarship. February 2007.
  • Societal Impact of Information Technologies: Fall 2018, Fall 2017 NEW
  • Introduction to Computer Science II, Honors: Spring 2018
  • Cloud-Scale Software Engineering: Spring 2017 (Yale).
  • Object-Oriented Programming: Fall 2014 (NYU).
  • Data Structures: Spring 2014 (NYU), Fall 2013 (NYU)
Thesis Examination
  • Thomas Dickerson (Brown), Thesis Examination, exp.
  • Kshitij Bansal (NYU), Thesis Examination, 2016
  • Paul Gazzillo (NYU), Thesis Examination, 2015
  • Jingyue Wu (Columbia), Thesis Examination, 2014
  • PhD, Computer Science, University of Cambridge, 2012. Gates Scholarship.
  • Sc.M, Computer Science, Brown University, 2008.
  • B.S., Highest Honors, Computer Science and Physics, College of William & Mary, 2001.
  • Assistant Professor, Stevens Institute of Technology
  • Lecturer and Research Scientist, Yale University
  • Research Staff Member, IBM TJ Watson Research Center
  • Research Scientist; Visiting Assistant Professor, New York University.
  • Visiting Professor, Nagoya University, Japan
  • Research Intern, Microsoft Research Cambridge & Redmond
  • Software Engineer at IMDb
Visits and Invited Talks
  • NYU, New York, Robust Concurrent Software from Commutativity & Atomicity, Dec 2016.
  • Columbia University, New York, Robust Concurrent Software from Commutativity & Atomicity, Nov 2016.
  • Boston University, Boston, Temporal Verification of Programs, Nov 2016.
  • NJPLS, Reversible Atomic Objects, Sep 2016.
  • NFSC-JSPS Joint Research Workshop, Proving Crash Recoverability. Kyoto. July 2015.
  • IBM PL Day, IBM Research, New York, The Push/Pull Model of Transactions, Nov 2014.
  • Microsoft Research, Cambridge, UK, Local Temporal Reasoning, July 2014.
  • University College, London, UK, Local Temporal Reasoning, July 2014.
  • Yale University, Local Temporal Reasoning, Mar 2014.
  • Rice University, Local Temporal Reasoning, Mar 2014.
  • Cornell University, Local Temporal Reasoning, Feb 2014.
  • IBM Research, New York, Local Temporal Reasoning, Feb 2014.
  • NYU, New York, Local Temporal Reasoning, Jan 2014.
  • Tokyo University, Japan, Temporal verification of programs, May 2013.
  • Nagoya University, Japan, Temporal verification of programs, Apr 2013.
  • ETH Zurich, Switzerland, Commutativity Race Detection, Feb 2013.
  • Queen Mary University, London, Specialization for Synchronization, Feb 2013.
  • NEC Research, Reasoning about Nondeterminism in Programs, Mar 2013.
  • Microsoft Research, A Theory of Serializabile Transactions, Nov 2012.
  • CMACS NSF PI Meeting, Reasoning about Nondeterminism in Programs, Oct 2012.
  • IBM PL Day, Reasoning about Nondeterminism in Programs, Jun 2012.
  • High Confidence Software and Systems, Reasoning about Nondeterminism in Programs, May 2012.
  • Vienna Sci. Tech. Fund, Austria, Data-structure Commutativity for Multicore Processing, Dec 2011.
  • NJPLS, Reasoning about Nondeterminism in Programs, Oct 2011.
  • IBM TJ Watson Research Lab, Systems Code Verification: A Moving Target, Apr 2011.
  • RiSE Seminar, IST Austria, Systems Code Verification: A Moving Target, Apr 2011.
  • Microsoft Research Cambridge, Systems Code Verification: A Moving Target, Mar 2011.
  • Oxford University, Branching-time reasoning for general-purpose programs, May 2010.
  • University of Maryland, Making prophecies with decision predicates, May 2010.
  • IBM TJ Watson Research Lab, Making prophecies with decision predicates, Feb 2010.
  • Sun Microsystems, Boston.
  • The College of William & Mary, Symbolic bound analysis, February 12, 2009.
  • Queen Mary University of London, Symbolic bound analysis, Dec 2008.
  • Microsoft Research, Symbolic bound analysis, September 2008.


Intellectual Property

I have served as a source code expert on several litigations, including patent infringement and trade secrets cases. Recently, I worked with the following firms and (respective) cases:

  • FitBit vs. Jawbone. Source Code Expert. Gibson Dunn, atty. ITC Investigation No. 337-TA-973.
  • Confluence, Intl. vs Minnesota Department of Transportation. Testifying Expert. Walsten & Te Slaa, attys.
  • (undisclosed), Source Code Expert, Trade Secrets case, 2014 - 2016.
  • Samsung vs. Ericsson. Kikland & Ellis LLP, atty. Source Code Expert, Mobile Phone Technology, Spring 2013 - Winter 2014. District Court Civil Action No. 6:12-cv-00894-LED.
  • Samsung vs. Ericsson. Kikland & Ellis LLP, atty. Source Code Expert, Mobile Phone Technology. ITC Investigation No. 337-TA-866. Samsung vs. Ericsson
  • Irell & Manella LLP, Source Code Expert, Winter 2013