| | Name:
Education:
Occupation:
CV:
Email:
Links: | Aleksandar Milicevic
Ph.D. in Computer Science from MIT
Founding Engineer at Cubist
milicevic-cv.pdf
[email protected]
DBLP, Google Scholar, LinkedIn, GitHub |
I am a Founding Engineer at Cubist, working on tooling for Web3, focusing on security, correctness, and ease of use.
Previously, I worked as a Principal Software Engineer at Microsoft where I led the development of various low-level Linux-specific solutions, like process sandboxing and filesystem virtualization. I was also a key contributor to a novel build system that leverages said solutions to automatically add caching and distribution to any existing build.
Broadly speaking, I am interested in developing tools and techniques that help software engineers build strong, robust, and reliable software systems more easily. I am particularly keen on fusing traditional programming languages and declarative programming techniques (e.g., constraint solving, lightweight formal specifications, model-driven development, model-based synthesis, etc.) to achieve said goals.
I received my PhD in Computer Science from MIT in 2015, advised by Prof. Daniel Jackson. My thesis---Advancing Declarative Programming---focuses on combining declarative and imperative programming paradigms into tools that simplify building complex software that is correct by design.
- Alloy*—a general-purpose, higher-order, relational constraint solver
- Sunny—a model-based, event-driven, policy-agnostic paradigm for developing reactive web applications.
- αRby—an embedding of Alloy in Ruby
- Squander—a framework for unified execution of imperative code and declarative first-order specifications
- Jennisys—a programming language and a synthesis tool from declarative first-order specifications to imperative code
- Alloy Analyzer—a model finder for a first-order relational specification language
- Korat—a tool for automated generation of structurally complex test inputs for Java programs
- Puzzler—a solver for natural-language logic puzzles
-
Unifying Execution of Imperative Generators and Declarative Specifications
P. Nie, M. Parovic, Z. Zang, S. Khurshid, A. Milicevic, M. Gligoric
OOPSLA 2020 -
Debugging the Performance of Maven’s Test Isolation: Experience Report
P. Nie, A. Çelik, M. Coley, A. Milicevic, J. Bell, M. Gligoric
ISSTA 2020, Los Angeles, USA; July 2020 -
VeDebug: Regression Debugging Tool for Java
Ben Buhse, Thomas Wei, Zhiqiang Zang, Aleksandar Milicevic, Milos Gligoric
ICSE 2019 Demo Montreal, Canada; May 2019 -
Regression Test Selection Across JVM Boundaries
A. Çelik, M. Vasic, A. Milicevic, M. Gligoric
FSE 2017 Paderborn, Germany; September 2017
[full text], [bibtex] -
File-level vs. Module-level Regression Test Selection for .NET
M. Vasic, Z. Parvez, A. Milicevic, M. Gligoric
(Industrial Paper) FSE 2017 Paderborn, Germany; September 2017
[full text], [bibtex] -
Multi-Representational Security Analysis
E. Kang, A. Milicevic, D. Jackson
FSE 2016 Seattle, WA, USA; November 2016
(distinguished paper award)
[abstract], [full text], [bibtex] -
Build System with Lazy Retrieval for Java Projects
A. Çelik, A. Knaust, A. Milicevic, M. Gligoric
FSE 2016 Seattle, WA, USA; November 2016
[abstract], [full text], [bibtex] -
Alloy*: A Higher-Order Relational Constraint Solver
A. Milicevic, J. P. Near, E. Kang, and D. Jackson -
Advancing Declarative Programming
A. Milicevic
Massachusetts Institute of Technology, PhD Thesis, May 2015.
[slides] [abstract] [full text] [bibtex] -
αRby—An Embedding of Alloy in Ruby
A. Milicevic, Ido Efrati, and D. Jackson
ABZ 2014 Toulouse, France; June 2014
[slides] [abstract] [full text] [bibtex] -
Model-Based, Event-Driven Programming Paradigm for Interactive Web Applications
A. Milicevic, M. Gligoric, D. Marinov, and D. Jackson
Onward! 2013 Indianapolis, IN, USA; October 2013
[slides] [poster] [abstract] [full text] [bibtex] -
Program Extrapolation with Jennisys
K. R. M. Leino, and A. Milicevic-
SPLASH 2012 Tucson, AZ, USA; October 2012
[abstract] [full text] [bibtex] -
MSR-TR 2012 Microsoft Technical Report; February 2012
[slides] [abstract] [full text] [bibtex]
-
-
Preventing Arithmetic Overflows in Alloy
A. Milicevic, and D. Jackson -
Unifying Execution of Imperative and Declarative Code
A. Milicevic, D. Rayside, K. Yessenov, and D. Jackson.
ICSE 2011 Waikiki, Honolulu, HI, USA; May 2011
[slides] [abstract] [full text] [bibtex] -
A Lightweight Approach to Construction and Evaluation of a Dependability Case
J. P. Near, A. Milicevic, E. Kang, D. Jackson.
ICSE 2011 Waikiki, Honolulu, HI, USA; May 2011
[abstract] [full text] [bibtex] -
Model Checking Using SMT and Theory of Lists
A. Milicevic, H. Kugler.
NFM 2011 Pasadena, CA, USA; April 2011
[example] [slides] [abstract] [full text] [bibtex] -
Executable Specifications for Java Programs
A. Milicevic
Massachusetts Institute of Technology, Master Thesis, September 2010
[slides] [abstract] [full text] [bibtex] -
Agile Specifications
D. Rayside, A. Milicevic, K. Yessenov, G. Dennis and D. Jackson
Onward! 2009 Orlando, FL, USA; October 2009
[abstract] [full text] [bibtex] -
Equality and Hashing for (almost) Free: Generating Implementations from Abstraction Functions
D. Rayside, Z. Benjamin, J. Near, R. Sing, A. Milicevic and D. Jackson
ICSE 2009 Vancouver, Canada; May 2009
[abstract] [full text] [bibtex] -
Parallel test generation and execution with Korat
S. Misailovic, A. Milicevic, N. Petrovic, S. Khurshid, and D. Marinov
ESEC/FSE 2007 Dubrovnik, Croatia; September 2007
[slides] [abstract] [full text] [bibtex] -
Korat: A Tool for Generating Structurally Complex Test Inputs
A. Milicevic, S. Misailovic, D. Marinov, and S. Khurshid
ICSE Demo 2007 Minneapolis, MN, USA; May 2007
[abstract] [full text] [bibtex] -
Generating Test Inputs for Fault-Tree Analyzers using Imperative Predicates
S.Misailovic, A.Milicevic, S.Khurshid, D.Marinov
STEP 07 Memphis, TN, USA; May 2007
[abstract] [full text] [bibtex]
title | school | department | major | date |
---|---|---|---|---|
PhD | MIT, Cambridge, MA, USA | EECS | Computer Science | 2010 - 2015 |
MSc | MIT, Cambridge, MA, USA | EECS | Computer Science | 2008 - 2010 |
BSc | University of Belgrade, Serbia | EECS | Computer Science | 2003 - 2007 |
High School | Mathematical Gymnasium, Belgrade, Serbia | Computer Science | 1999 - 2003 |
title | company | job description | date |
---|---|---|---|
Software Engineer | Microsoft, Redmond, WA, USA |
Developing a modern build system enabling fast, distributed, reliable, cacheable, incremental builds | Aug 2015 present |
Research Intern | Microsoft Research, Redmond, WA, USA |
Program synthesis from declarative first-order specifications | Jun 2011 Aug 2011 |
Research Intern | Microsoft Research, Cambridge, UK |
Bounded model checking using SMT and Theory of Lists (with application to analysis and execution of Live Sequence Charts) | Jun 2009 Aug 2009 |
Software Engineer | Serbian Object Laboratories, Belgrade, Serbia |
Developing a web-based enterprise information system using WebWork, Java Servlets, SOAP, JSP, HTML, CSS, JS, AJAX, Sybase IQ | Mar 2006 Aug 2008 |
Software Development Intern | Google, New York, NY, USA |
Barcode scanner for mobile devices (using computer vision, machine learning, Java ME on Symbian OS) | Jul 2007 Sep 2007 |
Research Intern | UIUC, Urbana, IL, USA |
Software testing, automatic test case generation with Korat, model checking with JPF | Aug 2006 Sep 2006 |
Windows Server 2003 Sys Admin (part-time) | School of Electrical Engineering, Belgrade, Serbia |
Maintenance and administration of a small computer network (30 client computers under Windows XP operating system and one server computer under Windows 2003 Server) for the lab and teaching purposes | Nov 2005 Feb 2007 |
Software Development Intern | Serbian Object Laboratories, Belgrade, Serbia |
Model driven development of Object Oriented Information Systems | Jul 2005 Aug 2005 |