Aleksandar Milicevic Home Page

Name: Education: Occupation: CV: Email: Links:

Aleksandar Milicevic Ph.D. in Computer Science from MIT Founding Engineer at Cubist milicevic-cv.pdf aleks@cubist.dev DBLP, Google Scholar, LinkedIn, GitHub

About Me

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.

Research Projects

• 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

Publications

1. Unifying Execution of Imperative Generators and Declarative Specifications
   P. Nie, M. Parovic, Z. Zang, S. Khurshid, A. Milicevic, M. Gligoric
   OOPSLA 2020

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

3. VeDebug: Regression Debugging Tool for Java
   Ben Buhse, Thomas Wei, Zhiqiang Zang, Aleksandar Milicevic, Milos Gligoric
   ICSE 2019 Demo Montreal, Canada; May 2019

4. Regression Test Selection Across JVM Boundaries
   A. Çelik, M. Vasic, A. Milicevic, M. Gligoric
   FSE 2017 Paderborn, Germany; September 2017
   [full text], [bibtex]

5. 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]

6. Multi-Representational Security Analysis
   E. Kang, A. Milicevic, D. Jackson
   FSE 2016 Seattle, WA, USA; November 2016
   (distinguished paper award)
   [abstract], [full text], [bibtex]

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

8. Alloy*: A Higher-Order Relational Constraint Solver
   A. Milicevic, J. P. Near, E. Kang, and D. Jackson
   

   • FMSD 2017 (journal paper)
     [abstract] [full text] [bibtex]

   • ICSE 2015 Florence, Italy; May 2015
     (distinguished paper award)
     [slides] [abstract] [full text] [bibtex]

   • MIT-TR-2014-018 MIT Technical Report; September 2014
     [abstract] [full text] [bibtex]

9. Advancing Declarative Programming
   A. Milicevic
   Massachusetts Institute of Technology, PhD Thesis, May 2015.
   [slides] [abstract] [full text] [bibtex]

10. α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]

11. 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]

12. 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]

13. Preventing Arithmetic Overflows in Alloy
    A. Milicevic, and D. Jackson

    • SCP 2014 (journal paper) May 2014.
      [abstract] [full text] [bibtex]

    • ABZ 2012 Pisa, Italy; June 2012
      [slides] [abstract] [full text] [bibtex]

14. 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]

15. 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]

16. 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]

17. Executable Specifications for Java Programs
    A. Milicevic
    Massachusetts Institute of Technology, Master Thesis, September 2010
    [slides] [abstract] [full text] [bibtex]

18. Agile Specifications
    D. Rayside, A. Milicevic, K. Yessenov, G. Dennis and D. Jackson
    Onward! 2009 Orlando, FL, USA; October 2009
    [abstract] [full text] [bibtex]

19. 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]

20. 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]

21. 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]

22. 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]

Education

Experience