Books

• Matt Kaufmann, Panagiotis Manolios, and J Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, July 2000.
  The latest version of the book (updated on January 2008) is available in paperback form from the just-in-time publisher lulu.

  This is the ACL2 textbook. ACL2 is part of the Boyer-Moore family of provers, for which Boyer, Kaufmann and Moore won 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.
  The latest version of the book (updated on January 2008) is available in paperback form from the just-in-time publisher lulu.

Dissertation

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

Edited Proceedings

• Aarti Gupta and Panagiotis Manolios, editors. Proceedings of the ACM/IEEE Formal Methods in Computer-Aided Design Conference. IEEE, November 2006.

• Panagiotis Manolios and Matthew Wilding, editors. Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications. ACM, August 2006.
  The proceedings are available in paperback form from the just-in-time publisher lulu.

Recent Publications

• Ankit Kumar, Max von Hippel, Panagiotis Manolios and Cristina Nita-Rotaru. Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers. 2024 IEEE Symposium on Security and Privacy (SP). May 2024.

• Ankit Kumar, Max von Hippel, Panagiotis Manolios and Cristina Nita-Rotaru. Verification of GossipSub in ACL2s. ACL2 2023, EPTCS. November 2023. (Best Student Paper, 1st Place)

• Andrew T. Walter, Ankit Kumar and Panagiotis Manolios. Proving Calculational Proofs Correct. ACL2 2023, EPTCS. November 2023. (Best Student Paper, 2nd Place (tie))

• Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru and Lenore Zuck. A Case Study in Analytic Protocol Analysis in ACL2s. ACL2 2023, EPTCS. November 2023. (Best Student Paper, 2nd Place (tie))

• Zixuan Chen, Panagiotis Manolios and Mirek Riedewald. Why Not Yet: Fixing a Top-k Ranking that Is Not Fair to Individuals. VLDB 2023, Proceedings of the VLDB Endowment. Volume 16, May 2023.

• Ankit Kumar, Andrew Walter and Panagiotis Manolios. Automated Grading of Automata with ACL2s. ThEdu'22, Electronic Proceedings in Theoretical Computer Science. 2022.

• Andrew T. Walter, David Greve and Panagiotis Manolios. Enumerative Data Types with Constraints. FMCAD 2022, Formal Methods in Computer-Aided Design. Oct 2022.

• Andrew T. Walter and Panagiotis Manolios. ACL2s Systems Programming. ACL2 2022. May 2022.

• Ankit Kumar and Panagiotis Manolios. Mathematical Programming Modulo Strings. FMCAD 2021, Formal Methods in Computer-Aided Design. Oct 2021.

• Benjamin Quiring and Panagiotis Manolios. GACAL: Conjecture-based Verification. TACAS 2020, Tools and Algorithms for the Construction and Analysis of Systems. Apr 2020.

• Andrew Walter, Benjamin Boskin, Seth Cooper and Panagiotis Manolios. Gamification of Loop-Invariant Discovery from Code. HCOMP 2019, Human Computation and Crowdsourcing. Oct 2019.

• Mitesh Jain and Panagiotis Manolios. Local and Compositional Reasoning for Optimized Reactive Systems. CAV, Computer-Aided Verification (CAV 2019). July 2019.

• Panagiotis Manolios, Kit Siu, Michael Noorman and Hongwei Liao. A Model-Based Framework for Analyzing the Safety of System Architectures. 65th Reliability and Maintainability Symposium. January 2019.

• Abha Moitra, Kit Siu, Andrew Crapo, Harsh Chamarthi, Michael Durling, Meng Li, Han Yu, Panagiotis Manolios and Michael Meiners. Towards Development of Complete and Conflict-Free Requirements. 26th IEEE International Requirements Engineering Conference. August 2018. (Best Industrial Innovation Paper Award)

• Maria Pittou, Panagiotis Manolios, Jan Reineke and Stavros Tripakis. Checking multi-view consistency of discrete systems with respect to periodic sampling abstractons. Science of Computer Programming. Vol. 167, 2018.

• Justin Slepak, Panagiotis Manolios and Olin Shivers. Rank Polymorphism Viewed as a Constraint Problem. 5th ACM Sigplan International Workshop on Libraries, Languages and Compilers for Array Programming. June 2018.

• Kit Siu, Abha Moitra, Panagiotis Manolios, Michael Durling, Andrew Crapo, Meng Li, Han Yu, Craig McMillan, Heber Herencia-Zapana, Mauricio Castillo-Effen, Shiraj Sen, Daniel Russell and Sundeep Roy. Flight Critical Software and Systems Development using ASSERT. IEEE/AIAA 36th Digital Avionics Systems Conference. September 2017. (Best of track, Best of session awards)

• Mitesh Jain and Panagiotis Manolios. A Refinement-Based Approach to Testing of Hardware and Low-level Software Designs. DAC, Design Automation Conference, Work-In-Progress Poster. June 2016.

• Mitesh Jain and Panagiotis Manolios. Proving Skipping Refinement with ACL2s. ACL2 2015 October 2015.

• Mitesh Jain and Panagiotis Manolios. Skipping Refinement. CAV, Computer-Aided Verification (CAV 2015) July 2015.

• Panagiotis Manolios, Jorge Pais and Vasilis Papavasileiou. The Inez Mathematical Programming Modulo Theories Framework. CAV, Computer-Aided Verification (CAV 2015) July 2015.

• Greg Eakman, Howard Reubenstein, Tom Hawkins, Mitesh Jain, and Panagiotis Manolios. Practical Formal Verification of Domain-Specific Language Applications. NFM, NASA Formal Methods (NFM 2015) April 2015.

• Panagiotis Manolios, Vasilis Papavasileiou, and Mirek Riedewald. ILP Modulo Data. FMCAD, Formal Methods in Computer-Aided Design (FMCAD 2014) October 2014.

• Eugene Goldberg and Panagiotis Manolios. Partial quantifier elimination. HVC 2014 2014.

• Eugene Goldberg and Panagiotis Manolios. Quantifier elimination by dependency sequents. Formal Methods in System Design August 2014.

• Eugene Goldberg and Panagiotis Manolios. Software for Quantifier Elimination in Propositional Logic. ICMS, 2014.

• Harsh Chamarthi, Peter C. Dillinger, and Panagiotis Manolios. Data Definitions in the ACL2 Sedan. ACL2, 2014.

• Justin Slepak, Olin Shivers, and Panagiotis Manolios. An Array-Oriented Language with Static Rank Polymorphism. ESOP, 2014. Springer. (Best Paper Award)

• Panagiotis Manolios and Vasilis Papavasileiou. ILP Modulo Theories. CAV, 2013. Springer.

• Panagiotis Manolios. Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities. ITP, 2013. Springer.

• Eugene Goldberg and Panagiotis Manolios. Quantifier Elimination via Clause Redundancy. FMCAD, 2013.

• Eugene Goldberg and Panagiotis Manolios. Quantifier Elimination by Dependency Sequents. FMCAD, 2012.

• Harsh Chamarthi, Peter C. Dillinger, Matt Kaufmann, and Panagiotis Manolios. Integrating Testing and Interactive Theorem Proving. ACL2, 2011.

• Harsh Chamarthi and Panagiotis Manolios. Automated Specification Analysis Using an Interactive Theorem Prover. FMCAD, 2011.

• Panagiotis Manolios and Vasilis Papavasileiou. Pseudo-Boolean Solving by Incremental Translation to SAT. FMCAD, 2011. Springer.

• Christine Hang, Panagiotis Manolios, and Vasilis Papavasileiou. Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints. CAV, 2011. Springer.

• Harsh Chamarthi, Peter Dillinger, Panagiotis Manolios, and Daron Vroon. The ACL2 Sedan Theorem Proving System. TACAS, 2011. Springer.

• Panagiotis Manolios and Vasilis Papavasileiou. Virtual Integration of Cyber-Physical Systems by Verification. AVICPS, 2010.

• Eugene Goldberg and Panagiotis Manolios. SAT-solving Based on Boundary Point Elimination. Haifa Verification Conference, Oct. 2010. Springer LNCS 6504.

• Panagiotis Manolios and Daron Vroon. Interactive Termination Proofs Using Termination Cores. Interactive Theorem Proving, July 2010. Springer LNCS 6172.

• Eugene Goldberg and Panagiotis Manolios. Boundary Points and Resolution. Advanced Techniques in Logic Synthesis, Optimizations and Applications 2010. Springer.

• Eugene Goldberg and Panagiotis Manolios. Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encodings. TAP: Tests and Proofs, July 2010. Springer LNCS 6143.

• Panagiotis Manolios and Sudarshan K. Srinivasan. Verifying Pipelines with BAT. Design and Verification of Microprocessor Systems for High-Assurance Applications, edited by David S. Hardin, March 2010. Springer.

• Peter C. Dillinger and Panagiotis Manolios. Fast, All-Purpose State Storage. SPIN 2009, 16th International SPIN Workshop on Model Checking of Software, June 2009. Springer LNCS 5578.

• Benjamin Chambers, Panagiotis Manolios, and Daron Vroon. Faster SAT Solving with Better CNF Generation. DATE 2009, Design Automation and Test in Europe, April 2009. IEEE.

• Panagiotis Manolios and Aaron Turon. All-Termination(T). TACAS 2009, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, March 2009. Springer LNCS 5505.

• Matthew Might and Panagiotis Manolios. A posteriori soundness for non-deterministic abstract interpretations. VMCAI 2009, Tenth International Conference on Verification, Model Checking, and Abstract Interpretation, January 2009. Springer LNCS 5403.

• Panagiotis Manolios and Sudarshan K. Srinivasan. Automatic Verification of Safety and Liveness for Pipelined Machines Using WEB Refinement. ACM Transactions on Design Automation of Electronic Systems, volume 13(3), article 45, 2008.

• Panagiotis Manolios and Sudarshan K. Srinivasan. A Refinement-Based Compositional Reasoning Framework for Pipelined Machine Verification. IEEE Transactions on VLSI Systems, volume 16(4), pages 353-364, 2008.

• Panagiotis Manolios. Automating the Assembly of Avionics Systems. AIAA Guidance, Navigation, and Control Conference. August 2008. (Invited)

• William G.J. Halfond, Alessandro Orso, and Panagiotis Manolios. WASP: Detecting and Preventing SQL Injection Attacks Using Positive Tainting and Syntax-Aware Evaluation. IEEE Transactions on Software Engineering, special issue on Software Engineering for Secure Systems, volume 34(1), pages 65-81, 2008.

• David A. Greve, Matt Kaufmann, Panagiotis Manolios, J S. Moore, Sandip Ray, Jose L. Ruiz-Reina, Rob Sumners, Daron Vroon, and Matthew Wilding. Efficient Execution in an Automated Reasoning Environment. Journal of Functional Programming, volume 18(1), pages 15-46, 2008.

• Panagiotis Manolios. Automating System Assembly of Aerospace Systems. The Sixth NASA Langley Formal Methods Workshop, April 2008.

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

• Panagiotis Manolios, Gayatri Subramanian, and Daron Vroon. Automating Component-Based System Assembly. ISSTA 2007, International Symposium on Software Testing and Analysis. 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. 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. 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.