Aleksandar Milicevic Home Page

Avatar Name:
Aleksandar Milicevic
Ph.D. in Computer Science from MIT
Founding Engineer at Cubist
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


  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

  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

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

  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]


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