University of Cambridge
Computer Laboratory
15 JJ Thomson Avenue
Cambridge CB3 0FD
United Kingdom
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
Submitted
- Abstraction Refinement for Separation Logic Program Analyses. With Mike Dodds and Stephen Magill. [pdf]
- Proof-Directed Parallelization Synthesis by Separation Logic. With Mike Dodds and Suresh Jagannathan. To appear in TOPLAS. [pdf]
Published
- 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]