## About

I am PhD student at the Programming, Logic, and Semantics Group of the University of Cambridge Computer Laboratory, supervised by Prof. Michael J. C. Gordon and Matthew Parkinson, and funded as a Gates Cambridge Scholar. I am also a honorary Trinity College External Research Scholar.

My research is aimed at developing ways for synthesising optimised software systems by using rigorous mathematical, formal analysis and verification techniques. I am particularly interested in such optimisations for concurrent, parallel and distributed systems, large-scale data processing systems, and energy-constrained systems such as mobile devices. In my PhD work, I was investigating novel approaches to automated parallelisation, by using separation logic, symbolic model checking and computational learning. I am generally interested in topics related to programming languages, concurrency, machine learning and systems.

My background is in mathematics and computer science, with a M.Sc degree in Mathematics from Faculty of Natural Sciences and Mathematics at University of Zagreb. Before I started my PhD, I worked on topics in combinatorial optimisation (path and routing problems) and applied mathematics (mathematical modelling and numerical simulations of partial differential equations).

My previous positions include:

- Visiting Research Scholar at Electrical Engineering and Computer Sciences, UC Berkeley
- Research Intern at Microsoft Research Cambridge
- Research Intern at Microsoft Research Redmond
- Research/Teaching Assistant at Department of Mathematics, University of Zagreb
- Various consulting and startup roles

## Papers

### Under submission

- Abstraction Refinement for Separation Logic Program Analyses. With Mike Dodds and Stephen Magill. [pdf]

### Published

- Proof-Directed Parallelization Synthesis by Separation Logic. With Mike Dodds and Suresh Jagannathan. ACM Trans. Program. Lang. Syst. 35(2): 8 (2013). [pdf]
- Sigma*: Symbolic Learning of Input-Output Specifications.
*Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13)*, 2013. With Domagoj Babic. [pdf] - Resource-Sensitive Synchronization Inference by Abduction.
*Proc. of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12)*, 2012. With Mike Dodds and Suresh Jagannathan. [pdf] - Safe Asynchronous Multicore Memory Operations.
*Proc. of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11)*, 2011. With Mike Dodds, Alastair F. Donaldson and Matthew J. Parkinson. [pdf] - coreStar: The Core of jStar.
*Proc. of the 1st International Workshop on Intermediate Verification Languages (Boogie 2011)*, 2011. With Dino Distefano, Mike Dodds, Radu Grigore, Daiva Naudziuniene and Matthew Parkinson. [pdf] - jStar-eclipse: an IDE for Automated Verification of Java Programs.
*Proc. of the 19th ACM International Symposium on Foundations of Software Engineering (FSE'11)*, 2011. With Daiva Naudziuniene, Dino Distefano, Mike Dodds, Radu Grigore and Matthew Parkinson. [pdf] - Automatic Safety Proofs for Asynchronous Memory Operations.
*Proc. of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'11)*, 2011. With Mike Dodds, Alastair F. Donaldson and Matthew J. Parkinson. [pdf] [pptx (poster)] - Separation Logic Verification of C Programs with an SMT Solver.
*Proc. of 4th International Workshop on Systems Software Verification (SSV'09)*, 2009. With Matthew J. Parkinson and Wolfram Schulte. [pdf] - Verification of Causality Requirements in Java Memory Model is Undecidable.
*Proceedings of 8th Int. Conf. on Parallel Processing and Applied Mathematics (PPAM 09), Workshop on Language-Based Parallel Programming Models*, 2009. With Paola Glavan and Davor Runje. [pdf]

### Other

- Symbolic Grey-Box Learning of Input-Output Relations.
*University of California, Berkeley Technical Report No. UCB/EECS-2012-59*, 2012. With Domagoj Babic and Dawn Song. [pdf] - Resource-Sensitive Synchronization Inference by Abduction (Extended Version).
*University of Cambridge, Computer Laboratory Report No. UCAM-CL-TR-808*, 2012. With Mike Dodds and Suresh Jagannathan. [pdf]