Eric Koskinen

Assistant Professor
Stevens Institute of Technology
(201) 216 5071 · eric.koskinen@stevens.edu

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.

Recent Activities

Nov 2018: Visiting UCL, Microsoft, Facebook. Joined the POPL 2020 PC
Aug 2018: Joined the OOPSLA 2019 PC and PLDI 2019 ERC.
Apr 2018: Cyrus Liu was accepted to OPLSS 2018.
Mar 2018: Our work on deductive fixpoint logic for temporal verification of higher-order programs was accepted to LICS 2018. NEW
Feb 2018: Our work on concurrent smart contracts was invited to the Bulletin of the EATCS. NEW
Jan 2018: Our paper was accepted to the Workshop on Trusted Smart Contracts.
Dec 2017: Our paper on Synthesizing Commutativity conditions [PDF] was accepted to TACAS 2018. NEW
Jul 2017: Joined the PODC 2018 program committee.
Jun 2017: Awarded a grant from the Office of Naval Research (ONR) involving automatic software verification. NEW
May 2017: Joined the PPoPP 2018 and VMCAI 2018 program committees.
Apr 2017: Our a new technique for parallelizing Ethereum Smart Contracts was accepted to PODC 2017.
Apr 2017: Delighted to announce that I am joining the faculty at Stevens Institute, effective August 2017!
Feb 2017: We have designed a new high-performance Scala-based TM implementation called Proust [web] [pdf]
Feb 2017: Our paper on Decomposing k-Safety for verifying absence of side-channel attacks was accepted to PLDI 2017.
Nov 2016: Our paper on Corrective Synchronization was accepted to VMCAI 2017.
July 2016: LICS 2016 was a success! Thanks to all who helped!
May 2016: Awarded a new NSF grant on verification and concurrency
Jan 2016: Presented our paper, Reducing Crash Recoverability to Reachability at POPL 2016. [Slides]

Continue to: Full List of Publication • Full List of Activities

Group

Ton Chanh Le, Research Scholar
Cyrus Liu, PhD student
Drew Malzahn, Master's
Feng Guo, Master's

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)

Opportunities

I am currently accepting applications for PhD students. 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 (eric.koskinen@stevens.edu) and submit an application via http://www.stevens.edu/ses/cs/graduate/doctorate.

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

Proof-Carrying Smart Contracts
Workshop on Trusted Smart Contracts (WTSC 2018)
Commutativity Condition Refinement
(EC2) 2015
Local Temporal Reasoning
HCSS 2014
Reasoning about nondeterminism in programs
HCSS 2012
Simplified Synchronization through Optimistic Linearizability
M Herlihy, E Koskinen.
What Theory for STM 2010
Concurrent Non-commutative Boosted Transactions
E Koskinen, M Herlihy.
TRANSACT 2009
Dreadlocks: Efficient Deadlock Detection
M Herlihy, E Koskinen
TRANSACT 2008
Checkpoints and Continuations instead of Nested Transactions
M Herlihy, E Koskinen.
TRANSACT 2008

Journals, Theses

How to add concurrency to smart contracts
T Dickerson, P Gazzillo, M Herlihy, E Koskinen.
Bulletin of the EATCS, No. 124
Temporal property verification as a program analysis task [Extended version]
Selected to appear in the CAV 2011 Special Issue.
B Cook, E Koskinen, M Vardi
FMSD 2012
Temporal verification of programs
E Koskinen
Doctoral Dissertation. University of Cambridge. 2012.

Projects

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)

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 Multicore Concurrency

Support from NSF (1618059 and 1421126)

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

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 in POPL 2016

Academic Activities

Service

OOPSLA 2019 program committee
PLDI 2019 exernal review committee
PODC 2018 program committee
PPoPP 2018 program committee
VMCAI 2018 program committee
LICS 2016 conference chair and steering committee
PPoPP 2016 external review committee
POPL 2016 external review committee
ECCOP 2016 external review committee
ICALP 2015 program committee
FMCAD 2014 external review committee
POPL 2013 program committee
SPAA 2012 program committee
OPODIS 2012 program committee
Yak International organizer

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.

Consulting

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