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 PhD work is focused on improving reliability of tricky pieces of software (often, concurrent or parallel) by static analysis and verification with separation logic. I am also investigating novel approaches to automated parallelisation, such as by using separation logic and computation learning. I am generally interested in topics related to programming languages, concurrency and software engineering.
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
New
- Sigma*: Symbolic Learning of Input-Output Specifications. With Domagoj Babic. To appear in POPL'13. [pdf]
Submitted
- Abstraction Refinement for Separation Logic Program Analyses. With Mike Dodds and Stephen Magill. [pdf]
- Resource-Sensitive Synchronization Inference by Abduction (Extended Version). With Mike Dodds and Suresh Jagannathan. [pdf]
Published
- 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]