Travelled to:1 × Estonia
1 × Japan
1 × Serbia
1 × Sweden
1 × United Kingdom
2 × Austria
2 × Denmark
7 × USA
Collaborated with:D.L.Dill C.W.Barrett I.Wehrman E.M.Westbrook P.Fu J.Carette L.Tan ∅ G.Sutcliffe C.Tinelli G.Kimmell R.E.H.Omar L.M.d.Moura D.Wu A.W.Appel D.Oe C.Oliver K.Clancy J.R.Levitt R.Besand J.C.Brodman J.Hseu B.Kinnersley G.T.Leavens J.Abrial D.S.Batory M.J.Butler A.Coglio K.Fisler E.C.R.Hehner C.B.Jones D.Miller S.L.P.Jones M.Sitaraman D.R.Smith
Talks about:type (5) checker (3) proof (3) framework (2) procedur (2) function (2) satisfi (2) languag (2) theori (2) modern (2)
Person: Aaron Stump
DBLP: Stump:Aaron
Contributed to:
2014
2014
2012
20122011
20062006
2005
20052005
2005
2003
200320022002
20012000Wrote 18 papers:
- IJCAR-2014-StumpST #framework #logic #named
- StarExec: A Cross-Community Infrastructure for Logic Solving (AS, GS, CT), pp. 367–373.
- RTA-TLCA-2014-FuS #encoding
- Self Types for Dependently Typed λ Encodings (PF, AS), pp. 224–239.
- PEPM-2012-CaretteS #towards #type system
- Towards typing for small-step direct reflection (JC, AS), pp. 93–96.
- VMCAI-2012-OeSOC #named #satisfiability
- versat: A Verified Modern SAT Solver (DO, AS, CO, KC), pp. 363–378.
- RTA-2011-StumpKO #confluence #problem
- Type Preservation as a Confluence Problem (AS, GK, REHO), pp. 345–360.
- GPCE-2006-LeavensABBCFHJMJSSS #roadmap #verification
- Roadmap for enhanced languages and methods to aid verification (GTL, JRA, DSB, MJB, AC, KF, ECRH, CBJ, DM, SLPJ, MS, DRS, AS), pp. 221–236.
- RTA-2006-WehrmanSW #named #termination
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker (IW, AS, EMW), pp. 287–296.
- CAV-2005-BarrettMS #contest #modulo theories #named #satisfiability
- SMT-COMP: Satisfiability Modulo Theories Competition (CWB, LMdM, AS), pp. 20–23.
- ICFP-2005-WestbrookSW #approach #imperative #programming
- A language-based approach to functionally correct imperative programming (EMW, AS, IW), pp. 268–279.
- RTA-2005-StumpT #algebra #proving #similarity
- The Algebra of Equality Proofs (AS, LYT), pp. 469–483.
- WRLA-2004-StumpBBHK05
- From Rogue to MicroRogue (AS, RB, JCB, JH, BK), pp. 69–87.
- CADE-2003-Stump #set
- Subset Types and Partial Functions (AS), pp. 151–165.
- PPDP-2003-WuAS #proving
- Foundational proof checkers with small witnesses (DW, AWA, AS), pp. 264–274.
- CADE-2002-StumpD #framework #logic #performance #proving
- Faster Proof Checking in the Edinburgh Logical Framework (AS, DLD), pp. 392–407.
- CAV-2002-BarrettDS #first-order #incremental #satisfiability
- Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (CWB, DLD, AS), pp. 236–249.
- CAV-2002-StumpBD #named
- CVC: A Cooperating Validity Checker (AS, CWB, DLD), pp. 500–504.
- LICS-2001-StumpBDL #array
- A Decision Procedure for an Extensional Theory of Arrays (AS, CWB, DLD, JRL), pp. 29–37.
- CADE-2000-BarrettDS #framework
- A Framework for Cooperating Decision Procedures (CWB, DLD, AS), pp. 79–98.