Panagiotis Manolios

107 papers A* 11A 16B 14C 1Journal 27Unranked 35
YearRankTypeTitle / 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