Eric Koskinen

Assistant Professor of Computer Science
Stevens Institute of Technology

e-mail: eric.koskinen@stevens.edu
phone: +1 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 Amazon.com.

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.

Group Members

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)

Recent Activities

Full List of Activities

Selected Publications

• Dependent Temporal Effects and a Fixpoint Logic for Verification NEW
Y Nanjo, H Unno, E Koskinen, T Terauchi.
LICS 2018
• Automatic Generation of Precise and Useful Commutativity Conditions [source] NEW
K Bansal, E Koskinen, O Tripp.
TACAS 2018
• Adding Concurrency to Smart Contracts NEW
T Dickerson, P Gazzillo, M Herlihy, E Koskinen.
PODC 2017
• 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
• Reducing Crash Recoverability to Reachability NEW
E Koskinen, J Yang
POPL 2016
• The Push/Pull model of transactions [Slides] [Extended]
E Koskinen, M Parkinson
PLDI 2015
• Local Temporal Reasoning [Full version]
E Koskinen, T Terauchi
CSL-LICS 2014
• Temporal property verification as a program analysis task [TR] [Slides]
B Cook, E Koskinen, M Vardi.
CAV 2011 Award paper

Full List of Publications

Publications

Drafts

• 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

Conferences

2018• Dependent Temporal Effects and a Fixpoint Logic for Verification 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.
OOPSLA 2013
 • 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

Workshops

Journals, Theses

Sample Projects

 

Proving Crash Recoverability

Problem
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.

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

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

 

Safety/Liveness Verification of Modern Languages

Problem
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.

Approach
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.

Accomplishments
• 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 Concurrency

Problem
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.

Approach
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.

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

 

Program Analysis for Complexity and Side-Channel attacks

Problem
Critical components of national cyberinfrastructure have been hardened to withstand traditional exploit-based attacks that target erroneous program behavior to compromise security. Looking forward such systems will be subject to a new class of attacks that do not rely on errors but rather exploit the inherent resource usage of the services the infrastructure provides. Such attacks have the potential to cripple critical service that are nonetheless correct. Program analysis has proved to be a powerful technique for detecting erroneous software behavior. However, termination/liveness, resource usage bounds, and side-channel capacity are increasingly difficult refinements of the basic program analysis problem. While some promising work exists, it fails to meet the requirements of speed and scale to the systematic analysis of large scale software systems and has not focused on the domain of exploitable resource usage patterns.

Approach
In a joint collaboration with the University of Maryland and Berkeley, we propose to investigate techniques and tools for the systematic and scalable human-aided, automated resource analysis of large scale software systems for which source code is not available.

Accomplishments
• Awarded a grant ($800,000) from DARPA
• Paper at PLDI 2017

Academic Activities

Service

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.

Teaching

  • 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

Education

  • 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.

Employment

  • 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 Amazon.com/ 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.

Consultation

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