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 Automated Verification, under the supervision of Prof. Marsha Chechik. After graduation I worked at JPL as a Software Engineer/Researcher. I am currently working as a Software Engineer in Lincoln, NE. Will no longer actively maintain this page.

ISoLA 2012 ISoLA 2012

NASA Formal Methods Symposium NFM 2011

Formal Aspects of Component Software Symposium FACS 2011

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