Zvonimir Rakamaric's Homepage

Business...

Zvonimir Rakamaric

Graduate Student
Department of Computer Science
University of British Columbia
2366 Main Mall
Vancouver, BC V6T 1Z4
Canada

email: email

My CV in pdf.

...and pleasure.

Aloha!
As you probably already figured out, my name is Zvonimir Rakamaric. Currently, I am a PhD student (I completed my MSc degree in August 2006) in the Department of Computer Science at UBC. My supervisor is Alan Hu. When I am at the department, I can usually be found in the Integrated Systems Design Lab, which is located in ICICS/CS room 342.
Down here you can find information about my academic life and other interesting things.

Research interests

Effective, automatic techniques for formal verification of complex systems and error detection
Verification of heap-manipulating programs
Model checking and abstraction techniques
Static program analysis and abstract interpretation

Publications

Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti: Verifying Heap-Manipulating Programs in an SMT Framework, 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), Tokyo, Japan
[pdf] [bib]
Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric: Proving Termination by Divergence, 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), London, UK
[pdf] [bib]
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti: Deciding Unbounded Heaps in an SMT Framework, Presentation-only paper, 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), Berlin, Germany
[abstract] [slides]
Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric: A Reachability Predicate for Analyzing Low-Level Software, 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), Braga, Portugal
Outstanding Student Paper Award sponsored by Microsoft Research Cambridge
[pdf] [bib]
Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric: A Reachability Predicate for Analyzing Low-Level Software, Microsoft Research Tech Report MSR-TR-2006-154, November 22, 2006
[pdf] [bib] [abstract]
Zvonimir Rakamaric, Jesse Bingham, Alan J. Hu: An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures, 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), Nice, France
[pdf] [bib]
Zvonimir Rakamaric: A Logic and Decision Procedure for Verification of Heap-Manipulating Programs, M.Sc. thesis, Department of Computer Science, The University of British Columbia, August, 2006
[pdf] [ps] [bib]
Zvonimir Rakamaric, Jesse Bingham, Alan J. Hu: A Better Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs, UBC Department of Computer Science Tech Report TR-2006-02, January 30, 2006
[pdf] [ps] [bib] [abstract]
Jesse Bingham, Zvonimir Rakamaric: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs, 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2006), Charleston, SC, USA
[pdf] [bib] [abstract]
Errata: After the paper was published, we found a bug in the implementation which slightly changes our experimental results. Our tech-report presents corrected results and adds proofs to the published version.
Jesse Bingham, Zvonimir Rakamaric: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs, UBC Department of Computer Science Tech Report TR-2005-19, September 19, 2005
[pdf] [bib] [abstract]
Domagoj Babic, Zvonimir Rakamaric: Bytecode Optimization, 24th International Conference on Information Technology Interfaces (ITI 2002), Cavtat, Croatia
[pdf] [bib]

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

Guidebook for Graduate Studies Abroad

Authors: Domagoj Babic, Zvonimir Rakamaric
Publisher: P.O.I.N.T.
ISBN: 978-953-99805-1-9
The main purpose of this guidebook in Croatian is to help people who seek top-quality education through graduate studies abroad. We hope that our knowledge and personal experience is going to help them to achieve their goals.
For a free paper edition of the guidebook contact kontakt@udruga-point.hr.
The latest online version of the guide is freely available and can be downloaded HERE.

In Croatian: Vodic za poslijediplomski studij u inozemstvu

Authori: Domagoj Babic, Zvonimir Rakamaric
Izdavac: P.O.I.N.T.
ISBN: 978-953-99805-1-9
Osnovna namjena ovog vodica je pomoci osobama koje su zainteresirane za vrhunsko obrazovanje kroz poslijediplomski studij u inozemstvu. Nadamo se da ce im nase znanje i osobno iskustvo pomoci da ostvare svoje ciljeve.
Za besplatno papirnato izdanje vodica kontaktirajte kontakt@udruga-point.hr.
Najnovija online verzija vodica je dostupna i moze se besplatno skinuti OVDJE.

Software

straclos decision procedure has been integrated into an available SMT solver MathSAT (big thanks to Roberto Bruttomesso and Alessandro Cimatti for helping out!). The new version of MathSAT extended with straclos (i.e. the theory of unbounded reachability) can be downloaded from the MathSAT homepage.
straclos 1.0 (Simple TRAnsitive CLOSure logic decision procedure) is available for download. We have been successfully using the decision procedure for predicate abstraction of heap-manipulating programs. You can download the source or Linux binary distribution, and try it out:
- straclos-1.0.tar.gz
- straclos-1.0-binary.tar.gz
Any feedback will be appreciated!

Links

I received the 2008 Microsoft Research Fellowship.
New!

Domagoj Babic's and mine 2 minutes of fame in science news on the Croatian National Television (HRT 1, February 14th). We talked about the Microsoft Research Fellowships we received. The entire interview can be seen on YouTube.
Formal verification and software analysis conferences and workshops
Formal verification (Wiki)
IEEE Spectrum: Why software fails
Wired: History's Worst Software Bugs
CNN/Money: Prius hybrids dogged by software
Study: Buggy software costs users, vendors nearly $60B annually
Embedded.com - Total Recall; Automotive industry software bugs

Fun Stuff

Betina Apartments
Krizevci - my hometown
Quotes and stuff...
Photos of Croatia
National Geographic Adventure ranks Croatia as the hottest 2006 destination
Photo Album
End Of Ze World