Jun 25 — Jul 5, 2009: Road Trip Through California, Nevada, Utah, and Arizona

• I took several days off before starting at a new position. My wife and I visited Yosemite, Death Valley, Las Vegas, Zion, Bryce Canyon, Coral Pink Sand Dunes, Grand Canyon, Hoover Dam, and Mojave Desert. Altogether, I drove 2350 miles (~3780 km), experienced temperatures from 40—117° Fahrenheit (5—47° Celsius), hiked on altitudes from -280 to 9000 ft (-85 to 2740 m), visited some of the most desolate and some of the busiest places in the US, swam in the ice-cold Merced river in Yosemite, and hiked upstream the Virgin River in the Zion park. In Grand Canyon, I saw two California condors, rare critically-endangered birds. In Vegas, I saw two great shows, the fantastically creative Mystere and the superb Phantom of the Opera. Free shows were also great: fledging twisters in the prairies of Arizona, a sunset over Bryce Canyon, and the fountain show in front of Bellagio. It was lots of fun. I might put some photos on the web site soon.

Jun 19, 2009: A New R&D Position

• Among several offers, I accepted a senior R&D position at Synopsys. I'm going to be working on an exciting guided random testing project. I'm starting at Synopsys on July 6th.
• This was also my last day consulting for Fujitsu Labs. It has been a great pleasure working with Sree Rajan and Mukul Prasad. The database testing project I've been working on has been very successful, and I managed to speed up the test case generation by 3—4 orders of magnitude and together with Mukul came up with some cool SMT encodings of frequently used database operations and data structures. I also did some interesting work on verification of web applications, JavaScript in particular.
• Sadly, I've heard a confirmation that Fujitsu will be closing the Maryland lab, leaving only the Sunnyvale lab open in the US. Hard times for everyone.

May 8, 2009: Spear Bug Reports

• Robert Brummeyer and Jonathan Heusser reported several bugs in Spear. I'll address these as soon as I find some time. My life is incredibly hectic these days, and seems like it's going to be so for the next couple of months.

Mar 13, 2009: Tour d'Europe

• I'll be interviewing in Europe from March 23rd to April 4th.
• Fujitsu Labs extended my consulting contract.

Feb 13, 2009: Consulting for Fujitsu Labs of America

• For the next month-or-so, I will be consulting for Fujitsu Labs. This is a part-time temporary contract, so it should leave me plenty of time for interviewing. I'll be working on an interesting problem in software analysis.

Jan 19 — 24, 2009: Attending POPL

• Attended POPL.

Jan 13, 2009: Dangerous Programming Bugs

• SANS published a list of 25 most dangerous programming bugs. Can't really say that any of the listed bugs surprised me.

Jan 7, 2009: Goodbye Cadence Research

• My last day on Cadence's payroll.

Nov 20, 2008: New Spear v1.9 Available

• Moved old news to a new page, Old News, to speed up loading of the main page.
• Evgeny fixed handling of SMT comments in smt2sf, new version is available for download (v1.9).

Nov 17, 2008: Updated SF2SMT Available

• Evgeny Pavlenko fixed a bug in sf2smt. The new version (v1.3) is now available. Thx Evgeny!

Nov 5, 2008: The Demise of Cadence Research Lab

• Cadence Research Lab killed. A number of researchers (including me) laid off, others assimilated into the product groups. I'm on the job market again.

Oct 28, 2008: New Spear Release

• New release (v2.7) of Spear: Fixed a really ugly bug in constant folding, reported by Evgeny Pavlenko. It's quite remarkable the bug remained undiscovered for so long. A big thanks to Evgeny!

Oct 23, 2008: SMT2SF Update

• New version of smt2sf released (v 1.8). Fixed a couple of warnings and a bug reported by Evgeny Pavlenko (thx!).

Oct 10, 2008: My Website Was Hacked!

• The main page was hacked... PmWiki seems to be less secure than I thought. Anyways, I did all I could to beef up security. Whoever hacked the page (seems like a bot from 89.149.244.45)... Can you please try again?

Oct 6, 2008: New SMT2SF

• New 1.7 release of smt2sf fixes a minor compilation problem on some platforms, reported by Johannes Waldmann (thx!).

Oct 2, 2008: Zvonimir and I Updated the Guide for Postgraduate Studies

• A new 2nd edition of the guide for postgraduate studies is now available. Check it out here.

Sep 1, 2008: Berkeley is My New Home

• Moved to Berkeley, CA.

Aug 25, 2008: Final Version of Domagoj's Thesis

• Final version of the thesis is now available on my publications page.

Aug 1, 2008: PhD Thesis Defense

• Defended my PhD thesis.

June 16, 2008: First Day at a New Position

• My first day of work for Cadence Research Laboratories. I'll be working from home (Vancouver, BC) until Sep 1st, when I'm moving to Berkeley, CA.

June 15, 2008: New Spear v2.6 Available

• New Spear v2.6 is available. Fixed a bug in constant folding of sign extension, reported by Trevor Alexander Hansen (Thx!). Also added Luby restarts and phase saving. Both new features are disabled for the time being (you can enable them with --hidden parameters). Tuning scripts have been updated as well.

May 12 — 18, 2008: Presenting a Paper at ICSE

• Attending ICSE in Leipzig.

Apr 28, 2008: Bit-Precise Reasoning Workshop Deadline Extended

• Due to multiple requests, the BPR paper submission deadline is extended till May 5th. Please submit the abstracts as soon as possible.

Apr 10, 2008: Joining a Research Lab

• I’m very happy to announce that I will be joining Cadence Research Lab in June! I’m going to continue working on decision procedures and software analysis. I’m moving to Berkeley in late August / early September.

Mar 6, 2008: New Spear v2.3 Available

• New Spear v2.3 is available. Three new sets of parameters are now available (thx to Frank). Also fixed a performance bug in the SF simplifier, reported by Greg Bronevetsky (thx Greg!).

Feb 22, 2008: Zvonimir and I on the Croatian National TV

• Zvonimir and I recently gave an interview to the Croatian National TV. The entire interview is available on YouTube and was aired in science news on Feb 14th on HRT 1.

Feb 13, 2008: Updated SMT2SF Available

• Levent Erkok from Galois discovered a minor glitch in smt2sf in interpretation of the SMT standard. This is now fixed in smt2sf 1.6. A big THX to Levent for reporting the issue.

Feb 11, 2008: Visiting Fortify Software

• Gave a talk about Calysto at Fortify Software in San Mateo. The company is focused on automatic software security analysis, which is a pretty cool problem.

Jan 23, 2008: New Website

• Frequent editing of the website became too much of a burden with the tools I was using, so I moved to PmWiki, which is a great tool! It will save me tons of time...

Jan 21, 2008: Leo and Nikolaj at UBC

• Leonardo de Moura and Nikolaj are visiting UBC on Fri, Jan 25th, and they are going to give two talks about their recent work. You can see the talk call here. If you want to talk to them in person, please sign up for a time slot [link].
• Bit-Precise Reasoning (BPR 2008) paper submission is now open!

Dec 10 — 15, 2007: Visiting SRI, UC Berkeley, Stanford, and Microsoft Research SVC

• Visited Shankar Natarajan at SRI. Gave a talk about bit-vector arithmetic.
• Visited Prof. Robert Brayton at UC Berkeley and gave the bit-vector arithmetic talk.
• Also visited Prof. David Dill at Stanford and gave the bit-vector arithmetic talk.
• Visited Lintao Zhang at Microsoft Research in Silicon Valley.

Nov 27 — Dec 11, 2007: Going Back Home...

• Trip to Zagreb. Spent some time with my family and friends and renewed my passport.
• Visited Faculty of Electrical Engineering and Computing at Zagreb University and gave a talk about automatic tuning of decision procedures. I also met with a bunch of students interested in pursuing postgraduate degrees abroad and spent 2 hours answering their questions .

Dec 5, 2007: Bit-Precise Reasoning Workshop

• Amit Goel from Intel Corporation and I are organizing a CAV-affiliated workshop on bit-precise reasoning. Today I set up the first BPR 2008 webpage. It's going to be a great workshop! Please consider submitting a paper.

Nov 17, 2007: Updated SMT2SF Available

• Levent Erkok from Galois discovered a bug in smt2sf. That has been fixed in the newly released smt2sf 1.5. Levent, thx for reporting it!

Nov 11 — 14, 2007: Presentation at FMCAD

• Attended FMCAD in Austin and presented a paper on automated tuning of decision procedures.

Nov 9, 2007: Visiting CMU

• Visited Prof. Edmund Clarke at Carnegie Mellon University and gave a talk at Specification and Verification Center weekly seminar.

Nov 8, 2007: Visiting SEI

• Visited Arie Gurfinkel and Sagar Chaki at Software Engineering Institute and gave a talk about reasoning about bit-vectors.

Nov 7, 2007: Visiting Harvard

• Visited Greg Morrisett at Harvard.

Nov 5 — 7, 2007: Visiting MIT

• Visited Felix Chang and gave a talk about reasoning about bit-vectors at MIT CSAIL.

Oct 20 — 26, 2007: A Trip to Israel

• Trip to Israel. Spent a bit of time sightseeing...
• Visited IBM in Haifa and gave a talk about automatic tuning of decision procedures.
• Presented a paper on exploiting shared structure in software verification conditions at Haifa Verification Conference

Oct 18, 2007: Visiting Intel

• Visiting Sava Krstic at Intel (Strategic CAD Labs), Portland.

Oct 17, 2007: New Spear v2.0 Available

• Release of Spear 2.0 (new front-end, completely rewritten common-subexpression elimination, new simplifier, fine-grained structural abstraction, and a few other unfinished analyses).

Sep 26, 2007: Visiting MPI in Saarbrucken

• Visited Andrey Rybalchenko at Max-Planck Institute and gave a talk there.
• Attended Dagstuhl (seminar 7401).

Sep 10 — 19, 2007: A Trip to the UK

• Attended SEFM in London and presented a paper on termination analysis of non-linear loops.
• Visited Wayne Luk at Imperial College in London, and presented some of my most recent work on automatic tuning of decision procedures.
• Visited Byron Cook at Microsoft Research Cambridge, and gave a talk there.
• Gave a talk at ARG Lunch at Cambridge University.

Sep 7, 2007: New Spear v1.4 Available

• Finally found time to make a new release of smt2sf 1.4, which includes a really nice patch submitted by Alberto Griggio (Thx!). The patch fixes a bug in conversion of some types of constraints.

Jul 31, 2007: Spear Wins one of the Categories on the SMT Competition

• Spear 1.9 wins on SMT bit-vector arithmetic division

Jun 25, 2007: Powerful New Parameter Configurations in Spear

• Release of new Spear 1.9. New release includes a powerful new fh_1_2 set of parameters and support for SMT-COMP output standard.

May 22, 2007: New Automatic Optimization Scripts

• Scripts for automatic optimization of Spear with ParamILS are now available.