Home Page of Panagiotis Manolios

Panagiotis (Pete) Manolios
Assistant Professor, College of Computing
Adjunct Assistant Professor, School of Electrical and Computer Engineering

Georgia Institute of Technology
266 Ferst Drive
Atlanta, Georgia 30332-0765 U.S.A.

Email:
Office:
Phone:
Fax:

manolios@cc.gatech.edu
KAC (Klaus Advanced Computing) 2340
+1 404 894 9219
+1 404 385 2295

News

We just released the BAT: The Bit-level Analysis Tool. BAT is a tool for deciding bounded model checking and k-induction queries for a powerful hardware description language that is strongly typed (with type inference), includes bit vectors, memories, and the standard operations on these data types, allows for user defined functions, functions which return multiple values, etc. BAT has been used to solve problems that cannot be handled by any other decision procedure we have tried. For example, BAT can prove that a 32-bit 5 stage pipelined machine model refines its ISA in approximately 2 minutes.
I co-chaired FMCAD 2006. It was a great conference and slides for the tutorials, invited talks, and conference papers are now available online.
The proceedings of ACL2 2006 are now available online. ACL2 2006 was part of FLoC 2006 and was hosted by the CAV 2006 and IJCAR 2006 conferences.
Are you a user of ACL2 or interested in learning how to use the theorem prover? Then definitely look at the ACL2s system we are developing. It features a modern graphical integrated development environment in Eclipse, levels appropriate for beginners through experts, state-of-the-art enhancements such as our recent improvements to termination analysis, etc.
Are you considering using a Bloom filter? Use my Bloom filter calculator to compute the optimal settings, determine false positive rates, and much more.

Research

I am an Assistant Professor in the College of Computing at the Georgia Institute of Technology and a member of both the SPARC group and CERCS, the Center for Experimental Research in Computer Systems. I received my Ph.D. in Computer Sciences at the University of Texas at Austin in 2001.

My main research interest is mechanized formal verification and validation of computing systems. What guides my research is the vision that formal methods can be used to revolutionize the design and implementation of highly reliable, robust, and scalable systems in a variety of important application areas, ranging from large component-based software systems to hardware systems to aerospace systems to computational biology to public health. My other areas of interest include programming languages, distributed computing, logic, software engineering, algorithms, computer architecture, aerospace, and pedagogy.

CV

Publications

Software

BAT: The Bit-level Analysis Tool: A tool for deciding bounded model checking and k-induction queries for a powerful hardware description language that is strongly typed (with type inference), includes bit vectors, memories, and the standard operations on these data types, allows for user defined functions, functions which return multiple values, etc. BAT has been used to solve problems that cannot be handled by any other decision procedure we have tried. For example, BAT can prove that a 32-bit 5 stage pipelined machine model refines its ISA in approximately 2 minutes. These examples and many more are included.
ACL2s: The ACL2 Sedan: Making formal reasoning more widely accessible.
Bloom filter calculator: Use it to compute optimal settings, determine false positive rates, and much more.
3Spin and X3Spin: Modified versions of the Spin model checker with advances in the efficiency, configurability, and usability of probabilistic explicit-state verification.
3Murphi: A modified version of the Murphi verifier with advances in the efficiency, configurability, and usability of probabilistic explicit-state verification.

Professional Service

IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2007), PC Member.
FMCAD 2007 - IEEE/ACM International Conference on Formal Methods in Computer-Aided Design , PC Member and Benchmark Chair.
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2007), PC Member.
SAT 2007 - The Tenth International Conference on Theory and Applications of Satisfiability Testing , PC Member.
IEEE/ACM Asia and South Pacific Design Automation Conference (ASP-DAC 2007), PC Member.
IEEE/ACM International Conference on Formal Methods in Computer-Aided Design (FMCAD 2006), Co-Chair.
IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2006), PC Member.
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Co-Chair.
ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2006), PC Member.
Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2005), PC Member.
International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), PC Member.
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), PC Member.
Computer-Aided Verification (CAV 2004), PC Member.
Computer-Aided Verification (CAV 2003), PC Member.
IEEE International Conference on Computer Design (ICCD 2002), PC Member.
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002), PC Member.
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2000), PC Member.
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 1999), Organizing Committee.

Funding

My research is currently funded by Boeing, IBM, NASA, and NSF. See my CV for the details.

Current PhD Students

Former Students

Gayatri Subramanian: Masters student (with thesis), graduated Spring 2006, currently at Oracle.

Courses

Last modified: Wed Mar 28 15:15:12 EDT 2007
manolios@cc.gatech.edu

College of Computing
Georgia Tech