Korat: A Tool for Generating Structurally Complex Test Inputs. - Aleksandar Milicevic; Sasa Misailovic; Darko Marinov; Sarfraz Khurshid (ICSE, 2007)

Parallel test generation and execution with Korat. - Sasa Misailovic; Aleksandar Milicevic; Nemanja Petrovic; Sarfraz Khurshid; Darko Marinov (ESEC/SIGSOFT FSE, 2007)

Equality and hashing for (almost) free: Generating implementations from abstraction functions. - Derek Rayside; Zev Benjamin; Rishabh Singh; Joseph P. Near; Aleksandar Milicevic; Daniel Jackson 001 (ICSE, 2009)

Agile specifications. - Derek Rayside; Aleksandar Milicevic; Kuat Yessenov; Greg Dennis; Daniel Jackson 001 (OOPSLA Companion, 2009)

Unifying execution of imperative and declarative code. - Aleksandar Milicevic; Derek Rayside; Kuat Yessenov; Daniel Jackson 001 (ICSE, 2011)

A lightweight code analysis and its role in evaluation of a dependability case. - Joseph P. Near; Aleksandar Milicevic; Eunsuk Kang; Daniel Jackson 001 (ICSE, 2011)

Model Checking Using SMT and Theory of Lists. - Aleksandar Milicevic; Hillel Kugler (NASA Formal Methods, 2011)

Program extrapolation with jennisys. - K. Rustan M. Leino; Aleksandar Milicevic (OOPSLA, 2012)

Model-based, event-driven programming paradigm for interactive web applications. - Aleksandar Milicevic; Daniel Jackson 001; Milos Gligoric 001; Darko Marinov (Onward!, 2013)

αRby - An Embedding of Alloy in Ruby. - Aleksandar Milicevic; Ido Efrati; Daniel Jackson 001 (ABZ, 2014)

Preventing arithmetic overflows in Alloy. - Aleksandar Milicevic; Daniel Jackson 001 (Sci. Comput. Program., 2014)

Advancing declarative programming. - Aleksandar Milicevic (2015)

Build system with lazy retrieval for Java projects. - Ahmet Çelik; Alex Knaust; Aleksandar Milicevic; Milos Gligoric 001 (SIGSOFT FSE, 2016)

Multi-representational security analysis. - Eunsuk Kang; Aleksandar Milicevic; Daniel Jackson 001 (SIGSOFT FSE, 2016)

Regression test selection across JVM boundaries. - Ahmet Çelik; Marko Vasic; Aleksandar Milicevic; Milos Gligoric 001 (ESEC/SIGSOFT FSE, 2017)

File-level vs. module-level regression test selection for .NET. - Marko Vasic; Zuhair Parvez; Aleksandar Milicevic; Milos Gligoric 001 (ESEC/SIGSOFT FSE, 2017)

VeDebug: regression debugging tool for Java. - Ben Buhse; Thomas Wei; Zhiqiang Zang; Aleksandar Milicevic; Milos Gligoric 001 (ICSE (Companion Volume), 2019)

Alloy*: a general-purpose higher-order relational constraint solver. - Aleksandar Milicevic; Joseph P. Near; Eunsuk Kang; Daniel Jackson 001 (Formal Methods Syst. Des., 2019)

Debugging the performance of Maven's test isolation: experience report. - Pengyu Nie 001; Ahmet Çelik; Matthew Coley; Aleksandar Milicevic; Jonathan Bell 001; Milos Gligoric 001 (ISSTA, 2020)

Unifying execution of imperative generators and declarative specifications. - Pengyu Nie 001; Marinela Parovic; Zhiqiang Zang; Sarfraz Khurshid; Aleksandar Milicevic; Milos Gligoric 001 (Proc. ACM Program. Lang., 2020)