|
Domagoj Babic |
|
Welcome to my page! I’m a PhD candidate at UBC. My research interests include: * Extended static checking * Software analysis, verification, and automated bug finding * Automated theorem proving (decision procedures) * SAT solving and constraint satisfaction in general * Design of digital systems (especially FPGA based ones) |
|
News: Apr 28, 08’ Due to multiple requests, the BPR paper submission deadline is extended till May 5th. Please submit the abstracts as soon as possible. Apr 10, 08’ 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, 08’ 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, 08’ - 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 21, 08’ - New Spear v2.2 is now available! It’s slightly faster, I fixed one performance bug that was around for a long time. Several new heuristics are now available. Feb 13, 08’ - 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, 08’ - 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 21, 08’ - Leonardo and Nikolaj are visiting UBC on Fri, Jan 25th, and they are going to give two talks about their recent work. Jan 21, 08’ - BPR paper submission is now open! Dec 10-15, 07’ - gave talks on reasoning about bit-vector arithmetic at SRI (visited Shankar), Berkeley (visited Prof. Brayton), and Stanford (visited Prof. Dill). Also visited Lintao Zhang at MSR. Dec 12, 07’ - our ICSE submission accepted for publication. Dec 6, 07’ - Gave a talk on automatic tuning of decision procedures at the Faculty of Electrical Engineering and Computing at Zagreb University Dec 5, 07’ - Created a web page for Bit-Precise Reasoning workshop (BPR)that I’m co-organizing with Amit Goel from Intel Corporation. BPR 2008 is affiliated with CAV 2008. Nov 17, 07’ - 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, 07’ - attended FMCAD in Austin, presented automatic tuning paper Nov 9, 07’ - visited Carnegie Mellon University and gave a talk at Specification and Verification Center weekly seminar Nov 8, 07’ - visited Arie Gurfinkel and Sagar Chaki at Software Engineering Institute and gave a talk about reasoning about bit-vectors Nov 7, 07’ - visited Greg Morrisett at Harvard Nov 5-7, 07’ - visited MIT CSAIL and gave a talk about my work Oct 07’ - visiting Sava Krstic at Intel, Portland Oct 17, 07’ - 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 - Oct 5, 07’ - Visiting Andrey Rybalchenko at Max-Planck Institute and gave a talk at Dagstuhl (seminar 7401) Sep 10 - 19, 07’ - Attending SEFM in London, visiting Byron at MSR, giving a talk at Arg lunch (Cambridge), and Imperial College. Sep 7, 07’ - 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. Aug 16, 07’ - Paper on exploiting shared structure in software verification conditions accepted at HVC Jul 31, 07’ - Spear 1.9 wins SMT bit-vector arithmetic section [link] Jun 25, 07’ - Release of Spear 1.9 (powerful new fh_1_2 set of parameters, support for SMT-COMP output standard). Jun 24, 07’ - Releases of Spear tools: autotune 1.2, smt2sf 1.3, sf2smt 1.2. Jun 21, 07’ - Paper on automatic optimization of decision procedures (with Frank Hutter, Holger Hoos, and Alan Hu) accepted at FMCAD. Jun 15, 07’ - Release of Spear 1.8 (several minor improvements). June 8, 07’ - Announced Calysto Community. May 30, 07’ - Paper on termination by divergence (with Alan, Zvonimir, and Byron) accepted at SEFM. May 22, ‘07 - Scripts for automatic optimization of Spear with ParamILS now available.
|
|
Home Page |
|
Domagoj Babic [pronunciation: mp3] The Department of Computer Science Tel: +1 (604) 822 4487 Fax: +1 (604) 822 5485 E-mail: my_last_name at cs.ubc.ca
My CV in [pdf]. |
|
Domagoj Babic |