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.
Recent Activities
|
Group
We are hiring talented PhD students to join us at Stevens! Please contact me if you are interested.
Previous Members
|
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.
• |
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 |
(Description forthcoming)
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.
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.
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
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: