Aaron Stump

Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli: SMT proof checking using a logical framework. Formal Methods in System Design 42(1): 91-118 (2013)

Clark Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump: 6 Years of SMT-COMP. J. Autom. Reasoning 50(3): 243-277 (2013)

Aaron Stump, Hans Zantema, Garrin Kimmell, Roba El Haj Omar: A Rewriting View of Simple Typing. Logical Methods in Computer Science 9(1) (2012)

Aaron Stump, Geoff Sutcliffe, Cesare Tinelli: Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. COMPARE 2012: 2

Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump: The 2nd Verified Software Competition: Experience Report. COMPARE 2012: 36-49

Jacques Carette, Aaron Stump: Towards typing for small-step direct reflection. PEPM 2012: 93-96

Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, Ki Yung Ahn: Equational reasoning about programs with general recursion and call-by-value semantics. PLPV 2012: 15-26

Duckki Oe, Aaron Stump, Corey Oliver, Kevin Clancy: versat: A Verified Modern SAT Solver. VMCAI 2012: 363-378

Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich: Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems. MSFP 2012: 112-162

Aaron Stump, Garrin Kimmell, Roba El Haj Omar: Type Preservation as a Confluence Problem. RTA 2011: 345-360

Clark Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli: The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference 2010: 3

Aaron Stump, Evan Austin: Resource typing in Guru. PLPV 2010: 27-38

Tim Sheard, Aaron Stump, Stephanie Weirich: Language-based verification will change the world. FoSER 2010: 343-348

Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich: Termination Casts: A Flexible Approach to Termination with General Recursion. PAR 2010: 76-93

Vilhelm Sjöberg, Aaron Stump: Equality, Quasi-Implicit Products, and Large Eliminations. ITRS 2010: 90-100

Aaron Stump: Proof Checking Technology for Satisfiability Modulo Theories. Electr. Notes Theor. Comput. Sci. 228: 121-133 (2009)

Aaron Stump: Directly reflective meta-programming. Higher-Order and Symbolic Computation 22(2): 115-144 (2009)

Aaron Stump, Evan Austin: Resource typing in guru: (abstract only). SIGPLAN Notices 44(11): 7 (2009)

Edwin M. Westbrook, Aaron Stump, Evan Austin: The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings. LFMTP 2009: 74-83

Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, Timothy W. Simpson: Verified programming in Guru. PLPV 2009: 49-58

Michael Zeller, Aaron Stump, Morgan Deters: Signature Compilation for the Edinburgh Logical Framework. Electr. Notes Theor. Comput. Sci. 196: 129-135 (2008)

Aaron Stump: Imperative LF Meta-Programming. Electr. Notes Theor. Comput. Sci. 199: 149-159 (2008)

Clark Barrett, Morgan Deters, Albert Oliveras, Aaron Stump: Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). International Journal on Artificial Intelligence Tools 17(4): 569-606 (2008)

Aaron Stump, Hongwei Xi: Preface. Electr. Notes Theor. Comput. Sci. 174(7): 1-2 (2007)

Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump: Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006). Formal Methods in System Design 31(3): 221-239 (2007)

Aaron Stump: Lightweight Verification with Dependent Types. VERIFY 2007

Aaron Stump, Hongwei Xi (Eds.): Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007. ACM 2007, isbn 978-1-59593-677-6

Ian Wehrman, Aaron Stump: Mining Propositional Simplification Proofs for Small Validating Clauses. Electr. Notes Theor. Comput. Sci. 144(2): 79-91 (2006)

Aaron Stump, Bernd Löchner: Knuth-Bendix completion of theories of commuting group endomorphisms. Inf. Process. Lett. 98(5): 195-198 (2006)

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: Roadmap for enhanced languages and methods to aid verification. GPCE 2006: 221-236

Ian Wehrman, Aaron Stump, Edwin M. Westbrook: Slothrop: Knuth-Bendix Completion with a Modern Termination Checker. RTA 2006: 287-296

Aaron Stump, Ryan Besand, James C. Brodman, Jonathan Hseu, Bill Kinnersley: From Rogue to MicroRogue. Electr. Notes Theor. Comput. Sci. 117: 69-87 (2005)

Aaron Stump, Carsten Schürmann: Logical Semantics for the Rewriting Calculus. Electr. Notes Theor. Comput. Sci. 125(2): 149-164 (2005)

Robert Klapper, Aaron Stump: Validated Proof-Producing Decision Procedures. Electr. Notes Theor. Comput. Sci. 125(3): 53-68 (2005)

Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump: Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005). J. Autom. Reasoning 35(4): 373-390 (2005)

Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump: SMT-COMP: Satisfiability Modulo Theories Competition. CAV 2005: 20-23

Edwin M. Westbrook, Aaron Stump, Ian Wehrman: A language-based approach to functionally correct imperative programming. ICFP 2005: 268-279

Aaron Stump, Li-Yang Tan: The Algebra of Equality Proofs. RTA 2005: 469-483

Aaron Stump: Programming with Proofs: Language-Based Approaches to Totally Correct Software. VSTTE 2005: 502-509

Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga: A Trustworthy Proof Checker. J. Autom. Reasoning 31(3-4): 231-260 (2003)

Aaron Stump: Subset Types and Partial Functions. CADE 2003: 151-165

Dinghao Wu, Andrew W. Appel, Aaron Stump: Foundational proof checkers with small witnesses. PPDP 2003: 264-274

Aaron Stump, Clark W. Barrett, David L. Dill: Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. Electr. Notes Theor. Comput. Sci. 70(2): 29-41 (2002)

Aaron Stump, David L. Dill: Faster Proof Checking in the Edinburgh Logical Framework. CADE 2002: 392-407

Clark W. Barrett, David L. Dill, Aaron Stump: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. CAV 2002: 236-249

Aaron Stump, Clark W. Barrett, David L. Dill: CVC: A Cooperating Validity Checker. CAV 2002: 500-504

Clark W. Barrett, David L. Dill, Aaron Stump: A Generalization of Shostak's Method for Combining Decision Procedures. FroCoS 2002: 132-146

Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt: A Decision Procedure for an Extensional Theory of Arrays. LICS 2001: 29-37

Clark W. Barrett, David L. Dill, Aaron Stump: A Framework for Cooperating Decision Procedures. CADE 2000: 79-98