Aleksandar Milicevic Home Page

This website is participating in a protest against the recently passed CISPA legislation.

In a nutshell: The U.S government and its law enforcement would be able to receive mountains of information from companies such as Facebook, Google, Twitter, and also your cell phone carrier simply by requesting it, no subpoena required. They would be able to use the information they gather for whatever purpose was deemed necessary, with NO LEGAL consequence.

Also important is that the scope of this bill is NOT confined to US residents. The US government would be able to get information about anyone in the world that has a Facebook, Google or Twitter account.

Name:Aleksandar Milicevic
Current Position: Software Engineer in the
Tools for Software Engineers group at
Microsoft
Email: almili@microsoft.com
aleks@csail.mit.edu
Web Home: http://people.csail.mit.edu/aleks/
CV: milicevic-cv.pdf
Links: DBLP,  Google Scholar,  LinkedIn

Past Projects

Publications

  • Advancing Declarative Programming [slides] [abstract] [full text] [bibtex]
    A. Milicevic
    Massachusetts Institute of Technology, PhD Thesis, May 2015.
  • Alloy*: A Higher-Order Relational Constraint Solver [website]
    A. Milicevic, J. P. Near, E. Kang, and D. Jackson
  • αRby—An Embedding of Alloy in Ruby [website] [slides] [abstract] [full text] [bibtex]
    A. Milicevic, Ido Efrati, and D. Jackson
    International Conference of Alloy, ASM, B, VDM, and Z Users (ABZ 2014), Toulouse, France, June 2014.
  • Model-Based, Event-Driven Programming Paradigm for Interactive Web Applications [slides] [poster] [abstract] [full text] [bibtex]
    A. Milicevic, M. Gligoric, D. Marinov, and D. Jackson
    OOPSLA Onward! (Onward! 2013, research paper), Indianapolis, Indiana, USA, October 2013.
  • Program Extrapolation with Jennisys [website]
    K. R. M. Leino, and A. Milicevic
  • Preventing Arithmetic Overflows in Alloy [website]
    A. Milicevic, and D. Jackson
  • Unifying Execution of Imperative and Declarative Code [website] [slides] [abstract] [full text] [bibtex]
    A. Milicevic, D. Rayside, K. Yessenov, and D. Jackson.
    33rd International Conference on Software Engineering (ICSE 2011), Waikiki, Honolulu, Hawaii, May 2011.
  • A Lightweight Approach to Construction and Evaluation of a Dependability Case [abstract] [full text] [bibtex]
    J. P. Near, A. Milicevic, E. Kang, D. Jackson.
    33rd International Conference on Software Engineering (ICSE 2011), Waikiki, Honolulu, Hawaii, May 2011.
  • Model Checking Using SMT and Theory of Lists [example] [slides] [abstract] [full text] [bibtex]
    A. Milicevic, H. Kugler.
    3rd NASA Formal Method Symposium (NFM 2011), Pasadena, California, April 2011.
  • Executable Specifications for Java Programs [slides] [abstract] [full text] [bibtex]
    A. Milicevic
    Massachusetts Institute of Technology, Master Thesis, September 2010.
  • Agile Specifications [abstract] [full text] [bibtex]
    D. Rayside, A. Milicevic, K. Yessenov, G. Dennis and D. Jackson
    OOPSLA Onward! (Onward! 2009, short paper), Orlando, Florida, USA, October 2009.
  • Equality and Hashing for (almost) Free: Generating Implementations from Abstraction Functions [abstract] [full text] [bibtex]
    D. Rayside, Z. Benjamin, J. Near, R. Sing, A. Milicevic and D. Jackson
    31st International Conference on Software Engineering (ICSE 2009), Vancouver, Canada.
  • Parallel test generation and execution with Korat [slides] [abstract] [full text] [bibtex]
    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, Sept. 2007.
  • Korat: A Tool for Generating Structurally Complex Test Inputs [website] [abstract] [full text] [bibtex]
    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, May 2007.
  • Generating Test Inputs for Fault-Tree Analyzers using Imperative Predicates [abstract] [full text] [bibtex]
    S.Misailovic, A.Milicevic, S.Khurshid, D.Marinov
    Workshop on Advances and Innovations in Systems Testing (STEP 07), Memphis, TN, May 2007.

Education

Experience

  • Full-time employee at Microsoft [August 2015 - present]
    Position:Software Engineer
  • Research internship at Microsoft Research, Redmond, WA, USA [June 2011 - August 2011]
    Position: Research Intern
    Host: Rustan Leino (leino@microsoft.com)
    Topic: Program synthesis from declarative first-order specifications
  • Research internship at Microsoft Research Cambridge, UK[June 2009 - August 2009]
    Position: Research Intern
    Host:Hillel Kugler (hkugler@microsoft.com)
    Topic:Analysis and execution of Live Sequence Charts with SMT solvers
  • Full-time employee at Serbian Object Laboratories [March 2006 - August 2008]
    Position:Software Engineer
    Job:Development of EDMT® Server using WebWork, Java Servlets, WS,
    SOAP, JSP, HTML, CSS, JS, AJAX, Sybase IQ
  • Summer internship at Google Inc. in New York [July 2007 - September 2007]
    Position:Software Engineering Intern
    Host:Nemanja Petrovic (nemanja@google.com)
    Topic:Computer vision, machine learning, development for mobile devices
  • Research internship at UIUC (the University of Illinois at Urbana Champaign) [August 2006 - September 2006]
    Position:Visiting Scholar
    Host:Prof. Darko Marinov (marinov@illinois.edu)
    Topic:Software testing, automatic test case generation and model checking
  • Part-time job at the School of Electrical Engineering in Belgrade [November 2005 - February 2007]
    Position:Windows Server 2003 system administrator
    Job: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.
  • Summer internship at Serbian Object Laboratories [July 2005]
    Position:Software Engineering Intern
    Host:Prof. Dragan Milicev (dragan.milicev@sol.rs)
    Topic:Model driven development of Object Oriented Information Systems
  • Summer job at a local computer-games playground [June 2003 - October 2003]
    Position:Network and system administrator
    Job:System and network administration of 10 networked computers running Windows XP

Teaching Activities

  • Teaching Assistant for "Elements of Software Construction" (undergraduate level course at MIT) in Spring'09 and Fall'09—gave recitations, graded problem sets and projects.
  • Lab Assistant for undergraduate courses in "Computer Architecture and Organization", "Operating Systems", "Data Structures" and "Pascal programming" at the School of Electrical Engineering in Belgrade—gave help and graded students.

Awards and Scholarships

  • College
    • Elektrijada 2006 - second place in the international competition of Schools of Electrical Engineering in Object Oriented Programming discipline. [May 2006]
    • Elektrijada 2005 - first place in the international competition of Schools of Electrical Engineering in two disciplines: Informatics and Object Oriented Programming. [May 2005]
    • Scholarship - EFG Eurobank Student Excellence Scholarship [2006/2007]
    • Scholarship - Government of the Republic of Serbia for Talented Senior Students [2006/2007]
    • Scholarship - Government of the City of Belgrade [2005/2006]
    • Scholarship - Government of the Republic of Serbia [2003/2004, 2004/2005, 2005/2006]
  • High School
    • all highest marks.
    • Scholarship - Government of the Republic of Serbia [2002/2003]
Aleksandar Milicevic
Last modified: Mon Sep 28 18:27:11 EDT 2015