Home Page of Panagiotis Manolios

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

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

Email:

pete@ccs.neu.edu

News

I moved to Northeastern University. My new webpage is here.

Research

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

pete@ccs.neu.edu