Panagiotis (Pete) Manolios Assistant Professor College of Computing Georgia Institute of Technology Email: manolios@cc.gatech.edu Phone: +1 404 894 9219

Books

• Matt Kaufmann, Panagiotis Manolios, and J Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, July 2000. In 2002, we released an updated paperback version that can be ordered here.

  This is the ACL2 textbook. ACL2 is part of the Boyer-Moore family of provers, winner of the 2005 ACM Software System Award.

• Matt Kaufmann, Panagiotis Manolios, and J Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, June 2000. In 2002, we released an updated paperback version that can be ordered here.

Dissertation

• Panagiotis Manolios. Mechanical Verification of Reactive Systems. The University of Texas at Austin, Department of Computer Sciences, Austin, TX, August 2001.

Recent Publications

• Panagiotis Manolios, Sudarshan Srinivasan, and Daron Vroon. BAT: The Bit-Level Analysis Tool. CAV 2007, Nineteenth International on Computer Aided Verification, to appear. July 2007.

• Panagiotis Manolios, Gayatri Subramanian, and Daron Vroon. Automating Component-Based System Assembly. ISSTA 2007, International Symposium on Software Testing and Analysis, to appear. July 2007.

• Panagiotis Manolios and Daron Vroon. Efficient Circuit to CNF Conversion. SAT 2007, The Tenth International Conference on Theory and Applications of Satisfiability Testing, to appear. May 2007.

• Peter Dillinger, Panagiotis Manolios, J Moore, Daron Vroon. ACL2s: "The ACL2 Sedan." ICSE 2007, The 29th International Conference on Software Engineering, Research Demonstration Track, to appear. May 2007.

• Panagiotis Manolios, Marc Galceran Oms, and Sergi Oliva Valls. Checking Pedigree Consistency with PCS. TACAS 2007, Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, March 2007.

• Panagiotis Manolios, Sudarshan K. Srinivasan, and Daron Vroon. Automatic Memory Reductions for RTL-Level Verification. ICCAD 2006, ACM-IEEE International Conference on Computer Aided Design, November 2006.

• Panagiotis Manolios and Sudarshan K. Srinivasan. A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures. Journal of Automated Reasoning, volume 37(1-2), pages 93-116, 2006.

• William G.J. Halfond, Alessandro Orso, and Panagiotis Manolios. Using Positive Tainting and Syntax-Aware Evaluation to Counter SQL Injection Attacks. Proceedings of the Fourteenth ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE 2006), November 2006.

• Panagiotis Manolios and Daron Vroon. Termination Analysis with Calling Context Graphs. Computer-Aided Verification (CAV-2006), part of FLoC'06, August 2006.

• Panagiotis Manolios and Yimin Zhang. Implementing Survey Propogation on Graphics Processing Units. International Conference on Theory and Applications of Satisfiability Testing (SAT-2006), part of FLoC'06, August 2006.

• Matt Kaufmann, Panagiotis Manolios, J Moore, and Daron Vroon. Integrating CCG Analysis into ACL2. The Eight International Workshop on Termination, part of FLoC'06, August 2006.

• Peter C. Dillinger, Panagiotis Manolios, J Moore, and Daron Vroon. ACL2s: "The ACL2 Sedan". Proceedigns of the 7th Workshop on User Interfaces for Theorem Proving, Electronic Notes in Theoretical Computer Science 174(2), pages 3-18, Elsevier 2007 (part of FLoC'06, August 2006).

• Panagiotis Manolios. Refinement and Theorem Proving. International School on Formal Methods for the Design of Computer, Communication, and Software Systems: Hardware Verification. Springer Verlag, LNCS Series, 2006.

• Panagiotis Manolios and Daron Vroon. Integrating Static Analysis and General-Purpose Theorem Proving for Termination Analysis. ICSE'06, The 28th International Conference on Software Engineering, Emerging Results, 2006.

• Panagiotis Manolios. Automating the Verification of RTL-Level Pipelined Machines. DCC'06, The Seventh International Workshop on Designing Correct Circuits, 2006.

• Roma Kane, Panagiotis Manolios, and Sudarshan K. Srinivasan. Monolithic Verification of Deep Pipelines with Collapsed Flushing. DATE 2006, ACM-IEEE Design, Automation, and Test in Europe, 2006.

• Panagiotis Manolios and Sudarshan K. Srinivasan. Verification of Executable Pipelined Machines with Bit-Level Interfaces. ICCAD 2005, ACM-IEEE International Conference on Computer Aided Design, November 2005.

• Panagiotis Manolios and Sudarshan K. Srinivasan. A Complete Compositional Reasoning Framework for the Efficient Verification of Pipelined Machines. ICCAD 2005, ACM-IEEE International Conference on Computer Aided Design, November 2005.

• Panagiotis Manolios. The Challenge of Hardware-Software Co-Verification. VSTTE, IFIP Working Conference on Verified Software: Theories, Tools, Experiments, Part of ETH's 150th anniversary celebration. Zurich, October 2005.

• Panagiotis Manolios and Daron Vroon. Ordinal Arithmetic: Algorithms and Mechanization. Journal of Automated Reasoning, volume 34(4), pages 387-423, 2005.

• Panagiotis Manolios and Sudarshan K. Srinivasan. A Computationally Efficient Method Based on Commitment Refinement Maps for Verifying Pipelined Machines. MEMOCODE 2005, ACM-IEEE International Conference on Formal Methods and Models for Codesign, 2005.

• Peter C. Dillinger and Panagiotis Manolios. Enhanced Probabilistic Verification with 3Spin and 3Murphi. SPIN 2005 12th International SPIN Workshop on Model Checking of Software, 2005.

• Panagiotis Manolios and Sudarshan K. Srinivasan. A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems. CHARME 2005, the 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 2005.

• Panagiotis Manolios and Sudarshan K. Srinivasan. Refinement Maps for Efficient Verification of Processor Models. DATE 2005, ACM-IEEE Design, Automation, and Test in Europe, 2005.

• Peter C. Dillinger and Panagiotis Manolios. Bloom Filters in Probabilistic Verification. FMCAD 2004, Formal Methods in Computer-Aided Design, 2004.

• Panagiotis Manolios and Daron Vroon. Integrating Reasoning about Ordinal Arithmetic into ACL2. FMCAD 2004, Formal Methods in Computer-Aided Design, 2004.

• Panagiotis Manolios and Sudarshan Srinivasan. A Suite of Hard ACL2 Theorems Arising in Refinement-Based Processor Verification. ACL2 2004, ACL2 Workshop, 2004.

• Marcio Gameiro and Panagiotis. Formally Verifying an Algorithm Based on Interval Arithmetic for Checking Transversality. ACL2 2004, ACL2 Workshop, 2004.

• Panagiotis Manolios and Sudarshan K. Srinivasan. Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements. DATE 2004, ACM-IEEE Design, Automation, and Test in Europe, 2004.

• Peter C. Dillinger and Panagiotis Manolios. Fast and Accurate Bitstate Verification for SPIN. SPIN 2004, 11th International SPIN Workshop on Model Checking of Software, 2004.

• Panagiotis Manolios and J Moore. Partial Functions in ACL2. Journal of Automated Reasoning, volume 31, issue 2, pages 107-127, 2003.

• Panagiotis Manolios. A Compositional Theory of Refinement for Branching Time. CHARME 2003, the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, October 2003.

• Panagiotis Manolios and Sudarshan K. Srinivasan. Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB-Refinements. CERCS TR# GIT-CERCS-03-17, September 2003.

• Panagiotis Manolios and Richard Trefler. A Lattice-Theoretic Approach to Safety and Liveness. Twenty-Second ACM Symposium on Principles of Distributed Computing (PODC 2003), pages 325-333. ACM Press, July 2003.

• Panagiotis Manolios. Branching Time Refinement. Brief Announcements, Twenty-Second ACM Symposium on Principles of Distributed Computing (PODC 2003), pages 334-334. ACM Press, July 2003.

• Panagiotis Manolios and Daron Vroon. Algorithms for Ordinal Arithmetic. Nineteenth International Conference on Automated Deduction (CADE), pages 243-257. Springer-Verlag, July 2003.

• Panagiotis Manolios and Daron Vroon. Ordinal Arithmetic in ACL2. Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July 2003.

• Panagiotis Manolios and Matt Kaufmann. Adding a Total Order to ACL2. The Third International Workshop on the ACL2 Theorem Prover, April 2002.

• Panagiotis Manolios and Richard J. Trefler. Safety and Liveness in Branching Time. Logic in Computer Science. LICS 2001, pages 366-374. IEEE Computer Society, June 2001.

• Panagiotis Manolios and J Moore. On the Desirability of Mechanizing Calculational Proofs. Information Processing Letters, volume 77(2-4), pages 173-179, 2001.

• Panagiotis Manolios. Verification of Pipelined Machines in ACL2. In J Moore and Matt Kaufmann, editors, ACL2 Workshop 2000. (See the companion FMCAD paper, below.)

• Panagiotis Manolios and J Moore. Partial Functions in ACL2. In J Moore and Matt Kaufmann, editors, ACL2 Workshop 2000.

• Panagiotis Manolios. Enumerating the Strings of a Regular Expression. Technical Report TR2000-30, Department of Computer Sciences, The University of Texas at Austin, December 2000.

• Panagiotis Manolios. Correctness of Pipelined Machines. In W. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer-Aided Design, FMCAD 2000, volume 1954 of LNCS, pages 161-178. Springer-Verlag, 2000. (See the companion ACL2 Workshop paper, above.)

• Panagiotis Manolios. Mu-Calculus Model-Checking. In Computer-Aided Reasoning: ACL2 Case Studies, pages 93-111. Kluwer Academic Publishers, May 2000.

• Panagiotis Manolios, Kedar Namjoshi, and Robert Sumners. Linking Theorem Proving and Model-Checking with Well-Founded Bisimulations. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification, CAV '99, volume 1633 of LNCS, pages 369-379. Springer-Verlag, 1999.

• Yuan Yu, Panagiotis Manolios, and Leslie Lamport. Model Checking TLA+ Specifications. In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods, CHARME '99, volume 1703 of LNCS, pages 54-66. Springer-Verlag, 1999.

• Panagiotis Manolios, Kedar Namjoshi, and Robert Sumners. Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation. Technical Report TR-99-02, University of Texas at Austin, Department of Computer Sciences, Austin, TX, January 1999. (Superseded by the CAV article.)

ACL2 Proof Scripts

• Panagiotis Manolios. Refinement and Theorem Proving . The proof scripts are described in the paper that appeared in the International School on Formal Methods for the Design of Computer, Communication, and Software Systems: Hardware Verification. Springer Verlag, LNCS Series, 2006. Tarred, Gzipped, 12K.

• Panagiotis Manolios and Daron Vroon. Ordinal Arithmetic in ACL2. The proof scripts are described in the ACL2 Workshop 2003 paper above and are also part of the ACL2 distribution starting with version 2.7. Tarred, Gzipped, 18K.

• Panagiotis Manolios and Matt Kaufmann. Adding a Total Order to ACL2. The proof scripts are described in the ACL2 Workshop 2002 paper, above. Tarred, Gzipped, 55K.

• Panagiotis Manolios. Verification of Pipelined Machines. The proof scripts are described in the FMCAD 2000 and ACL2 Workshop 2000 papers, above. Tarred, Gzipped, 92K.

• Panagiotis Manolios. Partial Functions in ACL2. The proof scripts are described in the ACL2 Workshop 2000 paper, above. Tarred, Gzipped, 21K.

• Panagiotis Manolios. Correctness Proof of Mu-Calculus Model-Checker. The proof scripts are described in the Mu-Calculus Model-Checking paper, above.

Last modified: Fri May 25 13:02:10 EDT 2007 manolios@cc.gatech.edu

Back to Pete's home page College of Computing