## Constantinos Bartzis## Postdoctoral FellowComputer Science Department, Carnegie Mellon University, Pittsburgh PA 15213 Email: cbartzis@cs.cmu.edu Phone: (412) 268-9873 Office: Wean Hall 7204 |

I received a
Diploma (B.S./M.Eng.) in Computer
Engineering and Informatics from the University of Patras, Greece in
1998 and a Ph.D. degree in Computer Science from the University of
California at Santa Barbara, under
the supervision of Prof. Tevfik
Bultan in 2004. Since October 2004 I am a Postdoctoral
Fellow in the
Model Checking Group at Carnegie
Mellon University, working with Prof. Edmund M. Clarke.

My research interests include software and hardware verification, symbolic and infinite state model checking, automata theory, computer security, decision procedures and parallel algorithms. In my Ph.D. Thesis I designed an automata-based symbolic representation for infinite-state model checking and developed efficient algorithms for symbolic manipulation, image computation and widening. I also solved a well known efficiency problem of BDD-based model checkers, due to their inability to represent arithmetic constraints concisely. At CMU I worked at various projects in Model Checking, Boolean Satisfiability and Computer Security.

My research interests include software and hardware verification, symbolic and infinite state model checking, automata theory, computer security, decision procedures and parallel algorithms. In my Ph.D. Thesis I designed an automata-based symbolic representation for infinite-state model checking and developed efficient algorithms for symbolic manipulation, image computation and widening. I also solved a well known efficiency problem of BDD-based model checkers, due to their inability to represent arithmetic constraints concisely. At CMU I worked at various projects in Model Checking, Boolean Satisfiability and Computer Security.