Panagiotis Manolios

107 papers A* 11A 16B 14C 1Journal 27Unranked 35

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	A Formalization of the Correctness of the Floodsub Protocol. ACL2 Ankit Kumar, Panagiotis Manolios
2025	—	`conf`	An ACL2s Interface to Z3. ACL2 Andrew T. Walter, Panagiotis Manolios
2025	—	`conf`	An Enumerative Embedding of the Python Type System in ACL2s. ACL2 Samuel Xifaras, Panagiotis Manolios, Andrew T. Walter, William Robertson
2025	J	`jnl`	Global Microprocessor Correctness in the Presence of Transient Execution. CoRR Andrew T. Walter, Konstantinos Athanasiou, Panagiotis Manolios
2025	—	`ed.`	Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, 12-13 May, 2025. ACL2 Ruben Gamboa, Panagiotis Manolios
2025	A*	`conf`	Synthesizing Scoring Functions for Rankings Using Symbolic Gradient Descent. ICDE Zixuan Chen, Panagiotis Manolios, Mirek Riedewald
2024	J	`jnl`	Finding Linear Explanations for a Given Ranking. CoRR Zixuan Chen, Panagiotis Manolios, Mirek Riedewald
2024	A*	`conf`	Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers. SP Ankit Kumar, Max von Hippel, Panagiotis Manolios, Cristina Nita-Rotaru
2024	—	`conf`	Instance-Optimized Mapping with Portfolio Methods. PACMI@SOSP Yibo Zhao, Panagiotis Manolios, Cheng Tan
2023	—	`conf`	A Case Study in Analytic Protocol Analysis in ACL2. ACL2 Max von Hippel, Panagiotis Manolios, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck
2023	J	`jnl`	Calculational Proofs in ACL2s. CoRR Andrew T. Walter, Ankit Kumar, Panagiotis Manolios
2023	—	`conf`	Proving Calculational Proofs Correct. ACL2 Andrew T. Walter, Ankit Kumar, Panagiotis Manolios
2023	—	`conf`	Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses. ACL2 Ruben Gamboa, Panagiotis Manolios, Eric Whitman Smith, Kyle Thompson
2023	—	`conf`	Verification of GossipSub in ACL2s. ACL2 Ankit Kumar, Max von Hippel, Panagiotis Manolios, Cristina Nita-Rotaru
2023	J	`jnl`	Why Not Yet: Fixing a Top-k Ranking that Is Not Fair to Individuals. Proc. VLDB Endow. Zixuan Chen, Panagiotis Manolios, Mirek Riedewald
2022	—	`conf`	ACL2s Systems Programming. ACL2 Andrew T. Walter, Panagiotis Manolios
2022	—	`conf`	Automated Grading of Automata with ACL2s. ThEdu@FLoC Ankit Kumar, Andrew T. Walter, Panagiotis Manolios
2022	B	`conf`	Enumerative Data Types with Constraints. FMCAD Andrew T. Walter, David A. Greve, Panagiotis Manolios
2021	J	`jnl`	A Reasoning Engine for the Gamification of Loop-Invariant Discovery. CoRR Andrew T. Walter, Seth Cooper, Panagiotis Manolios
2021	B	`conf`	Mathematical Programming Modulo Strings. FMCAD Ankit Kumar, Panagiotis Manolios
2020	—	`conf`	GACAL: Conjecture-Based Verification - (Competition Contribution). TACAS (2) Benjamin Quiring, Panagiotis Manolios
2019	J	`jnl`	Automating requirements analysis and test case generation. Requir. Eng. Abha Moitra, Kit Siu, Andrew W. Crapo, Michael Durling, Meng Li, Panagiotis Manolios, Michael Meiners, Craig McMillan
2019	B	`conf`	Gamification of Loop-Invariant Discovery from Code. HCOMP Andrew T. Walter, Benjamin Boskin, Seth Cooper, Panagiotis Manolios
2019	J	`jnl`	Introduction to Rank-polymorphic Programming in Remora (Draft). CoRR Olin Shivers, Justin Slepak, Panagiotis Manolios
2019	—	`conf`	Local and Compositional Reasoning for Optimized Reactive Systems. CAV (1) Mitesh Jain, Panagiotis Manolios
2019	—	`conf`	Records with rank polymorphism. ARRAY@PLDI Justin Slepak, Olin Shivers, Panagiotis Manolios
2019	J	`jnl`	The Semantics of Rank Polymorphism. CoRR Justin Slepak, Olin Shivers, Panagiotis Manolios
2018	J	`jnl`	Checking multi-view consistency of discrete systems with respect to periodic sampling abstractions. Sci. Comput. Program. Maria Pittou, Panagiotis Manolios, Jan Reineke, Stavros Tripakis
2018	—	`conf`	Rank polymorphism viewed as a constraint problem. ARRAY@PLDI Justin Slepak, Panagiotis Manolios, Olin Shivers
2018	A	`conf`	Towards Development of Complete and Conflict-Free Requirements. RE Abha Moitra, Kit Siu, Andrew W. Crapo, Harsh Raju Chamarthi, Michael Durling, Meng Li, Han Yu, Panagiotis Manolios, Michael Meiners
2017	J	`jnl`	An Efficient Runtime Validation Framework based on the Theory of Refinement. CoRR Mitesh Jain, Panagiotis Manolios
2015	—	`conf`	Practical Formal Verification of Domain-Specific Language Applications. NFM Greg Eakman, Howard Reubenstein, Tom Hawkins, Mitesh Jain, Panagiotis Manolios
2015	—	`conf`	Proving Skipping Refinement with ACL2s. ACL2 Mitesh Jain, Panagiotis Manolios
2015	—	`conf`	Skipping Refinement. CAV (1) Mitesh Jain, Panagiotis Manolios
2015	J	`jnl`	Skipping Refinement. CoRR Mitesh Jain, Panagiotis Manolios
2015	—	`conf`	The Inez Mathematical Programming Modulo Theories Framework. CAV (2) Panagiotis Manolios, Jorge Pais, Vasilis Papavasileiou
2014	A	`conf`	An Array-Oriented Language with Static Rank Polymorphism. ESOP Justin Slepak, Olin Shivers, Panagiotis Manolios
2014	J	`jnl`	Bug Hunting By Computing Range Reduction. CoRR Eugene Goldberg, Panagiotis Manolios
2014	—	`conf`	Data Definitions in the ACL2 Sedan. ACL2 Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios
2014	B	`conf`	ILP Modulo Data. FMCAD Panagiotis Manolios, Vasilis Papavasileiou, Mirek Riedewald
2014	J	`jnl`	ILP Modulo Data. CoRR Panagiotis Manolios, Vasilis Papavasileiou, Mirek Riedewald
2014	—	`conf`	Partial Quantifier Elimination. Haifa Verification Conference Eugene Goldberg, Panagiotis Manolios
2014	J	`jnl`	Partial Quantifier Elimination. CoRR Eugene Goldberg, Panagiotis Manolios
2014	J	`jnl`	Quantifier elimination by dependency sequents. Formal Methods Syst. Des. Eugene Goldberg, Panagiotis Manolios
2014	—	`conf`	Software for Quantifier Elimination in Propositional Logic. ICMS Eugene Goldberg, Panagiotis Manolios
2013	B	`conf`	Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities. ITP Panagiotis Manolios
2013	A*	`conf`	ILP Modulo Theories. CAV Panagiotis Manolios, Vasilis Papavasileiou
2013	B	`conf`	Quantifier elimination via clause redundancy. FMCAD Eugene Goldberg, Panagiotis Manolios
2013	J	`jnl`	Verification of Sequential Circuits by Tests-As-Proofs Paradigm. CoRR Eugene Goldberg, Mitesh Jain, Panagiotis Manolios
2012	J	`jnl`	Checking Satisfiability by Dependency Sequents CoRR Eugene Goldberg, Panagiotis Manolios
2012	J	`jnl`	ILP Modulo Theories CoRR Panagiotis Manolios, Vasilis Papavasileiou
2012	J	`jnl`	Quantifier Elimination by Dependency Sequents CoRR Eugene Goldberg, Panagiotis Manolios
2012	B	`conf`	Quantifier elimination by Dependency Sequents. FMCAD Eugene Goldberg, Panagiotis Manolios
2012	J	`jnl`	Removal of Quantifiers by Elimination of Boundary Points CoRR Eugene Goldberg, Panagiotis Manolios
2011	B	`conf`	Automated specification analysis using an interactive theorem prover. FMCAD Harsh Raju Chamarthi, Panagiotis Manolios
2011	—	`conf`	Integrating Testing and Interactive Theorem Proving ACL2 Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios
2011	B	`conf`	Pseudo-Boolean Solving by incremental translation to SAT. FMCAD Panagiotis Manolios, Vasilis Papavasileiou
2011	A*	`conf`	Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints. CAV Christine Hang, Panagiotis Manolios, Vasilis Papavasileiou
2011	A	`conf`	The ACL2 Sedan Theorem Proving System. TACAS Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios, Daron Vroon
2010	—	`conf`	Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding. TAP@TOOLS Eugene Goldberg, Panagiotis Manolios
2010	B	`conf`	Interactive Termination Proofs Using Termination Cores. ITP Panagiotis Manolios, Daron Vroon
2010	—	`conf`	SAT-Solving Based on Boundary Point Elimination. Haifa Verification Conference Eugene Goldberg, Panagiotis Manolios
2010	—	`ch.`	Verifying Pipelines with BAT. Design and Verification of Microprocessor Systems for High-Assurance Applications Panagiotis Manolios, Sudarshan K. Srinivasan
2009	B	`conf`	A PosterioriSoundness for Non-deterministic Abstract Interpretations. VMCAI Matthew Might, Panagiotis Manolios
2009	A	`conf`	All-Termination(T). TACAS Panagiotis Manolios, Aaron Turon
2009	—	`conf`	Fast, All-Purpose State Storage. SPIN Peter C. Dillinger, Panagiotis Manolios
2009	A	`conf`	Faster SAT solving with better CNF generation. DATE Benjamin Chambers, Panagiotis Manolios, Daron Vroon
2008	J	`jnl`	A Refinement-Based Compositional Reasoning Framework for Pipelined Machine Verification. IEEE Trans. Very Large Scale Integr. Syst. Panagiotis Manolios, Sudarshan K. Srinivasan
2008	J	`jnl`	Automatic verification of safety and liveness for pipelined machines using WEB refinement. ACM Trans. Design Autom. Electr. Syst. Panagiotis Manolios, Sudarshan K. Srinivasan
2008	J	`jnl`	Efficient execution in an automated reasoning environment. J. Funct. Program. David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding
2007	—	`conf`	ACL2s: "The ACL2 Sedan". ICSE Companion Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore
2007	A	`conf`	Automating component-based system assembly. ISSTA Panagiotis Manolios, Daron Vroon, Gayatri Subramanian
2007	A*	`conf`	BAT: The Bit-Level Analysis Tool. CAV Panagiotis Manolios, Sudarshan K. Srinivasan, Daron Vroon
2007	A	`conf`	Checking Pedigree Consistency with PCS. TACAS Panagiotis Manolios, Marc Galceran Oms, Sergi Oliva Valls
2007	A	`conf`	Efficient Circuit to CNF Conversion. SAT Panagiotis Manolios, Daron Vroon
2006	J	`jnl`	A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures. J. Autom. Reason. Panagiotis Manolios, Sudarshan K. Srinivasan
2006	—	`conf`	ACL2s: "The ACL2 Sedan". UITP@FLoC Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore
2006	A	`conf`	Automatic memory reductions for RTL model verification. ICCAD Panagiotis Manolios, Sudarshan K. Srinivasan, Daron Vroon
2006	A	`conf`	Implementing Survey Propagation on Graphics Processing Units. SAT Panagiotis Manolios, Yimin Zhang
2006	A*	`conf`	Integrating static analysis and general-purpose theorem proving for termination analysis. ICSE Panagiotis Manolios, Daron Vroon
2006	A	`conf`	Monolithic verification of deep pipelines with collapsed flushing. DATE Roma Kane, Panagiotis Manolios, Sudarshan K. Srinivasan
2006	—	`ed.`	Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006 ACL2 Panagiotis Manolios, Matthew Wilding
2006	—	`conf`	Refinement and Theorem Proving. SFM Panagiotis Manolios
2006	A*	`conf`	Termination Analysis with Calling Context Graphs. CAV Panagiotis Manolios, Daron Vroon
2006	—	`conf`	Using positive tainting and syntax-aware evaluation to counter SQL injection attacks. SIGSOFT FSE William G. J. Halfond, Alessandro Orso, Panagiotis Manolios
2005	—	`conf`	A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems. CHARME Panagiotis Manolios, Sudarshan K. Srinivasan
2005	A	`conf`	A complete compositional reasoning framework for the efficient verification of pipelined machines. ICCAD Panagiotis Manolios, Sudarshan K. Srinivasan
2005	C	`conf`	A computationally ef~cient method based on commitment re~nement maps for verifying pipelined machines. MEMOCODE Panagiotis Manolios, Sudarshan K. Srinivasan
2005	—	`conf`	Enhanced Probabilistic Verification with 3Spin and 3Murphi. SPIN Peter C. Dillinger, Panagiotis Manolios
2005	J	`jnl`	Ordinal Arithmetic: Algorithms and Mechanization. J. Autom. Reason. Panagiotis Manolios, Daron Vroon
2005	A	`conf`	Refinement Maps for Efficient Verification of Processor Models. DATE Panagiotis Manolios, Sudarshan K. Srinivasan
2005	—	`conf`	The Challenge of Hardware-Software Co-verification. VSTTE Panagiotis Manolios
2005	A	`conf`	Verification of executable pipelined machines with bit-level interfaces. ICCAD Panagiotis Manolios, Sudarshan K. Srinivasan
2004	A	`conf`	Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements. DATE Panagiotis Manolios, Sudarshan K. Srinivasan
2004	B	`conf`	Bloom Filters in Probabilistic Verification. FMCAD Peter C. Dillinger, Panagiotis Manolios
2004	—	`conf`	Fast and Accurate Bitstate Verification for SPIN. SPIN Peter C. Dillinger, Panagiotis Manolios
2004	B	`conf`	Integrating Reasoning About Ordinal Arithmetic into ACL2. FMCAD Panagiotis Manolios, Daron Vroon
2003	—	`conf`	A Compositional Theory of Refinement for Branching Time. CHARME Panagiotis Manolios
2003	A*	`conf`	A lattice-theoretic characterization of safety and liveness. PODC Panagiotis Manolios, Richard J. Trefler
2003	A	`conf`	Algorithms for Ordinal Arithmetic. CADE Panagiotis Manolios, Daron Vroon
2003	A*	`conf`	Brief announcement: branching time refinement. PODC Panagiotis Manolios
2003	J	`jnl`	Partial Functions in ACL2. J. Autom. Reason. Panagiotis Manolios, J Strother Moore
2001	J	`jnl`	On the desirability of mechanizing calculational proofs. Inf. Process. Lett. Panagiotis Manolios, J Strother Moore
2001	A*	`conf`	Safety and Liveness in Branching Time. LICS Panagiotis Manolios, Richard J. Trefler
2000	B	`conf`	Correctness of Pipelined Machines. FMCAD Panagiotis Manolios
1999	A*	`conf`	Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation. CAV Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers
1999	—	`conf`	Model Checking TLA CHARME Yuan Yu, Panagiotis Manolios, Leslie Lamport