Mihaela Bobaru (nee Gheorghiu)

I got my Ph. D. in Computer Science from the University of Toronto in March 2009. At U of T I worked in Formal Methods, since September 2003, under the supervision of Prof. Marsha Chechik. Now I have accepted an offer to join Gerard Holzmann's LaRS at JPL starting May 2010 (pending NASA approval).

Previously (2002) I got a Master of Mathematics in Computer Science at University of Waterloo under the supervision of Distinguished Prof. Emeritus John Brzozowski.

September 2008 -- December 2008

Research Intern at Microsoft Research, Cambridge, UK. Worked with Byron Cook.

September 2007 -- March 2008

Visiting Researcher at RIACS/NASA Ames, Mountain View, CA

Summers 2006 and 2007

Research Intern at NASA Ames, Mountain View, CA, working with Dimitra Giannakopoulou, Corina Pasareanu, Peter Mehlitz, Vandi Verma, Guillaume Brat, Bob Morris, and Michel Izygon (@ NASA Johnson Space Center, Houston, TX)

2002 - 2003

Lecturer at University of Nebraska - Lincoln in the Computer Science and Engineering Department.
Courses taught there:

CSCE-230 Computer Organization
CSCE-310 Data Structures and Algorithms
CSCE-252D FORTRAN Programming

Recent Publications

M. Gheorghiu Bobaru, C. S. Pasareanu, D. Giannakopoulou, Automated Assume-Guarantee Reasoning by Abstraction Refinement, in Proceedings of CAV 2008, July 2008, Princeton, NJ, USA.
C. S. Pasareanu, D. Giannakopoulou, M. Gheorghiu Bobaru, J. M. Cobleigh, H. Barringer, Learning to Divide-and-Conquer: Applying the L* Algorithm to Automate Assume-Guarantee Reasoning, in FMSD Journal, 37 pages, Springer OnlineFirst, January 2008.
M. Gheorghiu, A. Gurfinkel, M. Chechik, Finding State Solutions to Temporal Logic Queries, in Proceedings of IFM 2007 , Springer LNCS vol. 4591, pp. 273--292.
M. Gheorghiu, D. Giannakopoulou, C. Pasareanu, Refining Interface Alphabets for Compositional Verification, in Proceedings of TACAS 2007 , Springer LNCS vol. 4424, pp. 292--307.
M. Chechik, M. Gheorghiu, A. Gurfinkel, Finding Environment Guarantees, in Proceedings of FASE 2007 , Springer LNCS vol. 4422, pp. 352--367.
S. Nejati, M. Gheorghiu, M. Chechik, Thorough Checking Revisited, in Proceedings of FMCAD 2006 .

Other Publications

Tool Papers

M. Gheorghiu, A. Gurfinkel, VaqUoT: A Tool for Vacuity Detection, in Tools and Posters Track, FM 2006 .
M. Gheorghiu, A. Gurfinkel, TLQ: A Query Checker for States, in Tools and Posters Track, FM 2006.

Journal Papers

J. A. Brzozowski and M. Gheorghiu, Gate Circuits in the Algebra of Transients, Theoretical Informatics and Applications, Vol. 39, No. 1, pp. 67-91, January - March, 2005.
M. Gheorghiu and J. A. Brzozowski, Simulation of Feedback-Free Circuits in the Algebra of Transients, Int. J. Foundations of Computer Science, vol. 14, no. 6, pp. 1033-1054, December 2003.

Conference Papers

M. Gheorghiu and J. A. Brzozowski, Feedback-Free Circuits in the Algebra of Transients, Implementation and Application of Automata , J.-M. Champarnaud and D. Maurel, eds., (Revised papers from CIAA 2002, Tours, France, July 2002) Springer Lecture Notes in Computer Science, vol. 2608, pp. 106-116, June 2003. Copyright Springer-Verlag ( pdf )
J. A. Brzozowski and M. Gheorghiu, Simulation of Gate Circuits in the Algebra of Transients, Implementation and Application of Automata , J.-M. Champarnaud and D. Maurel, eds., (Revised papers from CIAA 2002, Tours, France, July 2002) Springer Lecture Notes in Computer Science, vol. 2608, pp. 57-66, June 2003. Copyright Springer-Verlag ( pdf )

Software

VaqUoT - a vacuity detector developed in the Formal Methods group here at U of T is available for download as a patch for the NuSMV model checker; the download is protected, but you are welcome to send me email at the address below and I will give you the user id and password.

Favourite Quote

"My gardener of chrysanthemums you are / Become their servant." Buson