_

Aleksandar Milicevic Home Page

Avatar Name:
Education:
Occupation:
Team:
Email:
Links:
Aleksandar Milicevic
Ph.D. in Computer Science from MIT
Software Engineer at Microsoft
Tools for Software Engineers (TSE)
almili@microsoft.com
DBLP, Google Scholar, LinkedIn, GitHub

About Me

I am a software engineer in the Tools for Software Engineers group at Microsoft. I am currently a member of the Build Tools team, working on a modern build system that enables fast, reliable, distributed, cacheable, incremental builds for projects ranging from single-developer apps to large-scale enterprise systems.

More broadly, 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 working with Prof. Daniel Jackson on Declarative Programming, Software Design, and Software Engineering in general.

Research Projects

  • Alloy*—a general-purpose, higher-order, relational constraint solver
  • α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. Regression Test Selection Across JVM Boundaries
    A. Çelik, M. Vasic, A. Milicevic, M. Gligoric
    11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2017] [to appear]
    Paderborn, Germany; September 2017

  2. File-level vs. Module-level Regression Test Selection for .NET
    M. Vasic, Z. Parvez, A. Milicevic, M. Gligoric
    (Industrial Paper) 11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2017] [to appear]
    Paderborn, Germany; September 2017

  3. Multi-Representational Security Analysis
    E. Kang, A. Milicevic, D. Jackson
    24th ACM SIGSOFT Foundations of Software Engineering (FSE 2016)
    Seattle, WA, USA; November 2016
    (distinguished paper award)
    [abstract], [full text], [bibtex]

  4. Build System with Lazy Retrieval for Java Projects
    A. Çelik, A. Knaust, A. Milicevic, M. Gligoric
    24th ACM SIGSOFT Foundations of Software Engineering (FSE 2016)
    Seattle, WA, USA; November 2016
    [abstract], [full text], [bibtex]

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

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

  7. αRby—An Embedding of Alloy in Ruby
    A. Milicevic, Ido Efrati, and D. Jackson
    International Conference of Alloy, ASM, B, VDM, and Z Users (ABZ 2014)
    Toulouse, France; June 2014
    [slides] [abstract] [full text] [bibtex]

  8. Model-Based, Event-Driven Programming Paradigm for Interactive Web Applications
    A. Milicevic, M. Gligoric, D. Marinov, and D. Jackson
    OOPSLA Onward! research paper (Onward! 2013)
    Indianapolis, IN, USA; October 2013
    [slides] [poster] [abstract] [full text] [bibtex]

  9. Program Extrapolation with Jennisys
    K. R. M. Leino, and A. Milicevic

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

  11. Unifying Execution of Imperative and Declarative Code
    A. Milicevic, D. Rayside, K. Yessenov, and D. Jackson.
    33rd International Conference on Software Engineering (ICSE 2011)
    Waikiki, Honolulu, HI, USA; May 2011
    [slides] [abstract] [full text] [bibtex]

  12. A Lightweight Approach to Construction and Evaluation of a Dependability Case
    J. P. Near, A. Milicevic, E. Kang, D. Jackson.
    33rd International Conference on Software Engineering (ICSE 2011)
    Waikiki, Honolulu, HI, USA; May 2011
    [abstract] [full text] [bibtex]

  13. Model Checking Using SMT and Theory of Lists
    A. Milicevic, H. Kugler.
    3rd NASA Formal Method Symposium (NFM 2011)
    Pasadena, CA, USA; April 2011
    [example] [slides] [abstract] [full text] [bibtex]

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

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

  16. Equality and Hashing for (almost) Free: Generating Implementations from Abstraction Functions
    D. Rayside, Z. Benjamin, J. Near, R. Sing, A. Milicevic and D. Jackson
    31st International Conference on Software Engineering (ICSE 2009)
    Vancouver, Canada; May 2009
    [abstract] [full text] [bibtex]

  17. Parallel test generation and execution with Korat
    S. Misailovic, A. Milicevic, N. Petrovic, S. Khurshid, and D. Marinov
    6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007)
    Dubrovnik, Croatia; September 2007
    [slides] [abstract] [full text] [bibtex]

  18. Korat: A Tool for Generating Structurally Complex Test Inputs
    A. Milicevic, S. Misailovic, D. Marinov, and S. Khurshid
    Formal Research Demo at the 29th International Conference on Software Engineering (ICSE Demo 2007)
    Minneapolis, MN, USA; May 2007
    [abstract] [full text] [bibtex]

  19. Generating Test Inputs for Fault-Tree Analyzers using Imperative Predicates
    S.Misailovic, A.Milicevic, S.Khurshid, D.Marinov
    Workshop on Advances and Innovations in Systems Testing (STEP 07)
    Memphis, TN, USA; May 2007
    [abstract] [full text] [bibtex]

Education

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

Experience

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