| 2018 | CPP | Generic derivation of induction for impredicative encodings in Cedille. | Denis Firsov, Aaron Stump |
| 2018 | ITP | Efficient Mendler-Style Lambda-Encodings in Cedille. | Denis Firsov, Richard Blair, Aaron Stump |
| 2014 | CADE | StarExec: A Cross-Community Infrastructure for Logic Solving. | Aaron Stump, Geoff Sutcliffe, Cesare Tinelli |
| 2012 | CADE | The 2nd Verified Software Competition: Experience Report. | Jean-Christophe Fillitre, Andrei Paskevich, Aaron Stump |
| 2012 | CADE | Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. | Aaron Stump, Geoff Sutcliffe, Cesare Tinelli |
| 2012 | PEPM | Towards typing for small-step direct reflection. | Jacques Carette, Aaron Stump |
| 2012 | VMCAI | versat: A Verified Modern SAT Solver. | Duckki Oe, Aaron Stump, Corey Oliver, Kevin Clancy |
| 2010 | CADE | Exploring Predictability of SAT/SMT Solvers. | Robert Brummayer, Duckki Oe, Aaron Stump |
| 2010 | ITP | Termination Casts: A Flexible Approach to Termination with General Recursion. | Aaron Stump, Vilhelm Sjberg, Stephanie Weirich |
| 2007 | CADE | Lightweight Verification with Dependent Types. | Aaron Stump |
| 2006 | GPCE | Roadmap for enhanced languages and methods to aid verification. | Gary T. Leavens, Jean-Raymond Abrial, Don S. Batory, Michael J. Butler, Alessandro Coglio, Kathi Fisler, Eric C. R. Hehner, Cliff B. Jones, Dale Miller, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump |
| 2005 | CAV | SMT-COMP: Satisfiability Modulo Theories Competition. | Clark W. Barrett, Leonardo Mendona de Moura, Aaron Stump |
| 2005 | ICFP | A language-based approach to functionally correct imperative programming. | Edwin M. Westbrook, Aaron Stump, Ian Wehrman |
| 2003 | CADE | Subset Types and Partial Functions. | Aaron Stump |
| 2003 | PPDP | Foundational proof checkers with small witnesses. | Dinghao Wu, Andrew W. Appel, Aaron Stump |
| 2002 | CADE | Faster Proof Checking in the Edinburgh Logical Framework. | Aaron Stump, David L. Dill |
| 2002 | CAV | Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. | Clark W. Barrett, David L. Dill, Aaron Stump |
| 2002 | CAV | CVC: A Cooperating Validity Checker. | Aaron Stump, Clark W. Barrett, David L. Dill |
| 2001 | LICS | A Decision Procedure for an Extensional Theory of Arrays. | Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt |
| 2000 | CADE | A Framework for Cooperating Decision Procedures. | Clark W. Barrett, David L. Dill, Aaron Stump |