Eric Koskinen |  |
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.
Note: Now Hiring Postdoctoral Researchers and PhD Students. Click here for details. NEW
Recent Work on Commutativity Verification
Other Recent Activities
Recent Service
|
Group
We are hiring talented PhD students to join us at Stevens! Please contact me if you are interested.
Previous Members
|
Opportunities
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 (eric.koskinen@stevens.edu) and submit an application via http://www.stevens.edu/ses/cs/graduate/doctorate.
Publications
Journals
-
Synthesizing Precise and Useful Commutativity Conditions
K Bansal, E Koskinen, O Tripp.
To appear in the special issue on TACAS 2018 in the Journal of Automated Reasoning (JAR 2020) - Adding Concurrency to Smart Contracts
T Dickerson, P Gazzillo, M Herlihy, E Koskinen.
In Distributed Computing (DIST 2020). - 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
Conferences
| 2021 | • |
Towards Optimal Use of Exception Handling Information for
Function Detection NEW C Pang, R Yu, D Xu, E Koskinen, G Portokalidis, J Xu DSN 2021 | |
| • |
SoK: All You Ever Wanted to Know About Binary Disassembly But Were Afraid to Ask NEW C Pang, R Yu, Y Chen, E Koskinen, G Portokalidis, B Mao, J Xu S&P 2021 | ||
| • |
Decomposing Data Structure Commutativity Proofs with mn-Differencing NEW
[slides]
[tool]
[youtube]
E Koskinen, K Bansal VMCAI 2021 | ||
| 2020 | • |
DynamiTe: Dynamic Termination and Non-termination Proofs NEW T-C Le, T Antonopoulos, P Fathololumi, E Koskinen, T Nguyen OOPSLA 2020 | |
| 2019 | • |
Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects [PDF] [ScalaProust • GitHub] T Dickerson, E Koskinen, M Herlihy, P Gazzillo APLAS 2019 | |
| • |
Specification and Inference of Trace Refinement Relations
[Knotical • GitHub] T Antonopoulos, E Koskinen, T Le OOPSLA 2019 |  |
|
| 2018 | • |
Dependent Temporal Effects and a Fixpoint Logic for Verification [Slides] Y Nanjo, H Unno, E Koskinen, T Terauchi. LICS 2018 | |
| • |
Automatic Generation of Precise and Useful Commutativity Conditions K Bansal, E Koskinen, O Tripp. TACAS 2018 |  |
|
| 2017 | • |
Adding Concurrency to Smart Contracts 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 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 |
Drafts
| • |
Reducing Commutativity Verification to Reachability with Differencing Abstractions E Koskinen, K Bansal CoRR. April 2020. | ||
| • |
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 |
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 -
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
Theses
- Temporal verification of programs
E Koskinen
Doctoral Dissertation. University of Cambridge. 2012.
Projects
Automatic Verification of Temporal Alignment (AVTA)
(Description forthcoming)
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 Multicore 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
• 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
- OOPSLA 2021 external review committee
- POPL 2020 program committee
- 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
- 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)
- 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 Amazon.com/ IMDb
- SRI International, New York, Concurrent Smart Contracts with Commutatiity & Atomicity, Mar 2019
- 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
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