Eric Koskinen
Associate Professor
Charles V. Schaefer, Jr. School of Engineering and Science
Department of Computer Science
Education
- PhD (2013) University of Cambridge (Computer Science)
- MS (2008) Brown University (Computer Science)
- BS (2001) The College of William and Mary (Computer Science and Physics)
Research
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.
Experience
I am an Associate 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.
Institutional Service
- Tenure-Track Faculty Hiring Committee Member
- CS P&T Committee Member
- Intellectual Property Advisory Committee Member
- Junior Faculty Board of Representatives - 21/22 Member
- Research & Entrepreneurship Committee Chair
- Search Committee for Non-Tenure Track Faculty Member
- Search Committee for the position of Vice Provost for Research and Innovation Member
- Search Committee for the position of Chair of the Computer Science Department Member
- Junior Faculty Board of Representatives Member
- Search Committee for the position of Vice Provost for Research and Innovation Member
- Faculty Panel for the Vice President for Information Technology and CIO Search Member
- Ribbon Cutting Ceremony for the Gateway Academic Center Member
- Curriculum Reorganization Committee Member
- Faculty Hiring Committee Member
Professional Service
- POPL 2025 Program Committe Program Committee Member
- Verification Mentoring Workshop at CAV 2024 Co-organizer of the Verification Mentoring Workshop at CAV 2024
- PLDI 2024 Program Committe Program Committee Member
- Verification Mentoring Workshop at CAV 2023 Co-organizer of the Verification Mentoring Workshop at CAV 2023
- Dutch Research Council (NWO) Panelist
- NETYS 2023 Program Committe Program Committee Member
- PLDI 2023 Program Committe Program Committee Member
- 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023) Program Committee Member
- 20th Asian Symposium on Programming Languages and Systems (APLAS 2022) Program Committee Member
- National Science Foundation Panelist
- 1st Workshop on Commutativity Reasoning (Commute 2022), co-located with PLDI 2022 Organizer
- National Science Foundation Reviewer
- OOPSLA 2021 Program Committee External Review Committee
- POPL 2020 Program Committe Program Committee Member
- OOPSLA 2019 Program Committee Program Committee Member
- Logic and Mentoring Workshop at LICS 2019 Co-organizer of the Logic and Mentoring Workshop at LICS 2019
- PLDI 2019 External Review Committee External Review Committee Member
- Review Panel at the National Science Foundation NSF Panel Member
Appointments
• Associate Professor, Stevens Institute of Technology
• 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, Amazon.com/ IMDb
• 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, Amazon.com/ IMDb
Honors and Awards
Charles Berendsen Junior Professorship, Fall 2021.
Provost's Early Career Award for Research Excellence.
Provost's Early Career Award for Research Excellence.
Professional Societies
- ACM/SIGPLAN Member
- ACM Member
- ACM Member
- SIGPLAN Member
Grants, Contracts and Funds
• Jul 2023 -- NSF Award on Verifying Concurrent Objects. $593k. With École Polytechnique, FR.
• Aug 2022 -- ONR award to continue work on the AVTA project. $215k.
• Jun 2021 -- NSF Award on Dynamic Temporal Analysis. $399k. With Yale and George Mason University.
• Jun 2020 -- NSF Award on Commutativity Analysis. $495k.
• Oct 2017 -- ONR award to study temporal logic-based automatic software verification. $3.2M.
• Jun 2016 -- NSF Award to work on verification of concurrent systems. $250k.
• Dec 2014 -- DARPA award to study complexity analysis. $800k.
• Jun 2014 -- NSF Award to work on concurrent languages and verification. $250k.
• Jun 2014 -- Office of the Provost, New York University. $ 17,000.
• Sep 2012 -- Japan Society for Promotion of Science (JSPS). 1,000,000 JPY.
• Aug 2022 -- ONR award to continue work on the AVTA project. $215k.
• Jun 2021 -- NSF Award on Dynamic Temporal Analysis. $399k. With Yale and George Mason University.
• Jun 2020 -- NSF Award on Commutativity Analysis. $495k.
• Oct 2017 -- ONR award to study temporal logic-based automatic software verification. $3.2M.
• Jun 2016 -- NSF Award to work on verification of concurrent systems. $250k.
• Dec 2014 -- DARPA award to study complexity analysis. $800k.
• Jun 2014 -- NSF Award to work on concurrent languages and verification. $250k.
• Jun 2014 -- Office of the Provost, New York University. $ 17,000.
• Sep 2012 -- Japan Society for Promotion of Science (JSPS). 1,000,000 JPY.
Selected Publications
Conference Proceeding
- Chen, A.; Fathololumi, P.; Koskinen, E.; Pincus, J. (2022). Veracity: Declarative Multicore Programming with Commutativity. Proceedings of the ACM on Programming Languages (PACMPL, OOPSLA 2022 Issue). Proceedings of the ACM on Programming Languages (PACMPL, OOPSLA 2022 Issue) (OOPSLA 2022 ed.).
https://www.erickoskinen.com/papers/veracity.pdf. - Liu, Y. C.; Pang, C.; Dietsch, D.; Koskinen, E.; Le, T. C.; Portokalidis, G.; Xu, J. (2021). Proving LTL Properties of Bitvector Programs and Decompiled Binaries. Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS).
- Liu, Y.; Pang, C.; Dietsch, D.; Koskinen, E.; Le, T.; Portokalidis, G.; Xu, J. (2021). Proving LTL of Bitvector Programs and Decompiled Binaries. The 19th Asian Symposium on Programming Languages and Systems (APLAS 2021). The 19th Asian Symposium on Programming Languages and Systems (APLAS 2021).
- Pang, C.; Yu, R.; Xu, D.; Koskinen, E.; Portokalidis, G.; Xu, J. (2021). Towards Optimal Use of Exception Handling Information for Function Detection. Proceedings of the IEEE/IFIP International Conference on Dependable Systems and Networks (DSN).
- Pang, C.; Yu, R.; Chen, Y.; Koskinen, E.; Portokalidis, G.; Mao, B.; Xu, J. (2021). SoK: All You Ever Wanted to Know About x86/x64 Binary Disassembly But Were Afraid to Ask. Proceedings of the IEEE Symposium on Security and Privacy.
- Pang, C.; Yu, R.; Chen, Y.; Koskinen, E.; Portokalidis, G.; Mao, B.; Xu, J. (2021). SoK: All You Ever Wanted to Know About Binary Disassembly But Were Afraid to Ask. Hoboken: The 41st IEEE Symposium on Security and Privacy (IEEE S&P 2021).
- Unno, H.; Terauchi, T.; Koskinen, E.. Constraint-based Relational Verification. International Conference on Computer Aided Verification (CAV 2021). International Conference on Computer Aided Verification (CAV 2021).
- Koskinen, E.; Bansal, K. (2021). Decomposing Data Structure Commutativity Proofs with mn-Differencing. Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021). Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021).
www.erickoskinen.com/papers/cityprover.pdf. - Dickerson, T.; Herlihy, M.; Koskinen, E.; Gazzillo, P. (2019). Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects. Proceedings of the 17th Asian Symposium on Programming Languages and Systems (APLAS). APLAS 2019.
https://www.cs.stevens.edu/~ejk/papers/proust.pdf. - Antonopoulos, T.; Le, T.; Koskinen, E. (2019). Specification and Inference of Trace Refinement Relations. Proceedings of the ACM on Programming Languages, Volume 2 (OOPSLA). OOPSLA 2019.
Journal Article
- Nagasamudram, R.; Koskinen, E.; Naumann, D. A. (2023). An algebra of alignment for relational verification. Proceedings of the ACM Programming Languages (POPL ed., vol. 7, pp. 574-603). ACM Press.
https://arxiv.org/abs/2202.04278. - Le, T.; Antonopoulos, T.; Fathololumi, P.; Koskinen, E.; Nguyen, T. (2020). DynamiTe: Dynamic Termination and Non-Termination Proofs. Proceedings of the ACM on Programming Languages (OOPSLA). New York, NY: ACM.
- Bansal, K.; Koskinen, E.; Tripp, O.. Synthesizing Precise and Useful Commutativity Conditions. Journal of Automated Reasoning. Springer.
- Dickerson, T.; Gazzillo, P.; Herlihy, M.; Koskinen, E. (2019). Adding concurrency to smart contracts. Distributed Computing.
https://doi.org/10.1007/s00446-019-00357-z.
Courses
• CS135: Discrete Structures. F'23.
• CS516: Compiler Design & Implementation: S'20, S'21, S'22, S'23, S'24.
• CS485: Societal Impact of Information Technologies: F'17, F'18, F'19, F'20, F'21, F'22, F'24.
• CS282: Introduction to Computer Science II, Honors: S'18.
• CS101: Research & Entrepreneurship in Computing: F'24.
• Object-Oriented Programming (at NYU): F'14
• Data Structures (at NYU): F'13, S'14.
• CS516: Compiler Design & Implementation: S'20, S'21, S'22, S'23, S'24.
• CS485: Societal Impact of Information Technologies: F'17, F'18, F'19, F'20, F'21, F'22, F'24.
• CS282: Introduction to Computer Science II, Honors: S'18.
• CS101: Research & Entrepreneurship in Computing: F'24.
• Object-Oriented Programming (at NYU): F'14
• Data Structures (at NYU): F'13, S'14.