Aleksandar Milicevic Home Page

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

Aleksandar Milicevic Ph.D. in Computer Science from MIT Previously Founding Engineer at Cubist milicevic-cv.pdf aca.milicevic@gmail.com, aleks@csail.mit.edu DBLP, Google Scholar, LinkedIn, GitHub

About Me

I am a security-focused systems engineer with a strong background in formal methods and over a decade of experience building and operating production infrastructure.

Most recently, I was a Founding Engineer at Cubist, where I co-designed CubeSigner, a hardware-backed, non-custodial platform for managing cryptographic keys that secures billions of dollars in digital assets. Keys are only ever handled inside AWS Nitro Enclaves, and the platform is built in Rust for low latency and high throughput. I was the main contributor to its declarative policy engine, which lets users state exactly when their keys may be used (spending limits, allowlists, time windows, multi-party approval), and I designed Rust “guard” types that make it a compile-time error to reach sensitive data without passing every required check. I also built the platform’s live monitoring and alerting, and managed two small engineering teams.

Before that, I spent seven years at Microsoft, most recently as a Principal Software Engineer, where I was tech lead for a range of low-level systems, including process sandboxing for Linux and macOS and filesystem virtualization for Linux. I integrated these into a distributed build system that significantly sped up Windows and Office builds.

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