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 for Fiserv. 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. |

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

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

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)

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

- 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*.

- 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.*

- 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.

- 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 )

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.

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