I do research in static analysis of software systems. My objectives are to

• design programming languages,
• engineer compilers, and
• create software analysis tools

that help programmers prove or improve

• performance,
• parallelism,
• security, and
• correctness.

I run the U Combinator software systems research group.

Research themes

Over time, a few themes have emerged in my research:

• flow analysis of higher-order languages;
• small-step abstract interpretation;
• methods that improve speed, precision and power in static analysis;
• taming the worst-case complexity of static analysis; and
• the art/science of designing/engineering a static analyzer.

Publications

• CiteULike: [my pubs] [my library]

Proceedings papers

1. (New) Christopher Earl, Matthew Might and David Van Horn. ``Pushdown control-flow analysis of higher-order programs: Precise, polyvariant and polynomial-time.'' 2010 Workshop on Scheme and Functional Programming. (Scheme 2010). Montreal, Quebec, Canada. August, 2010.
   
2. (New) David Van Horn and Matthew Might. ``Abstracting Abstract Machines.'' Accepted to International Conference on Functional Programming 2010 (ICFP 2010). Baltimore, Maryland. September, 2010.
   Paper: [pdf]
3. (New) Matthew Might. ``Abstract interpreters for free.'' Accepted to Static Analysis Symposium 2010 (SAS 2010). Perpignan, France. September, 2010.
   Paper: [pdf]
   
4. (New) Matthew Might, Yannis Smaragdakis and David Van Horn. ``Resolving and exploiting the k-CFA paradox: Illuminating functional vs. object-oriented program analysis.'' Programming Language Design and Implementation 2010 (PLDI 2010). Toronto, Canada. June, 2010. pages 305--315.
   Paper: [pdf] [bib]
   Slides: [pdf]
   

   @InProceedings{might2010mcfa,
     author =       {Matthew Might and Yannis Smaragdakis and David Van Horn},
     title =        {Resolving and exploiting the k-CFA paradox: Illuminating functional vs. object-oriented program analysis.},
     booktitle =    {Proceedings of the 31st {C}onference on {P}rogramming {L}anguage {D}esign and {I}mplementation  ({PLDI} 2006)},
     year =         {2010},
     pages =        {305--315},
     address =      {Toronto, Canada},
     month =        {June}
   }
   

5. (New) Matthew Might. ``Shape analysis in the absence of pointers and structure.'' 11th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2010). Madrid, Spain. January, 2010. pages 263--278.
   Paper: [pdf] [bib]
   Slides: [pdf] [www/html] [www/flash] [keynote]
   

   @InProceedings{might2010shape,
     author =       {Matthew Might},
     title =        {Shape analyis in the absence of pointers and structure},
     booktitle =    {Proceedings of the 11th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation  ({VMCAI} 2010)},
     year =         {2010},
     pages =        {263--278},
     address =      {Madrid, Spain},
     month =        {January}
   }
   

6. Matthew Might and Tarun Prabhu. ``Interprocedural dependence analysis of higher-order programs via stack reachability.'' 2009 Workshop on Scheme and Functional Programming. (Scheme 2009). Boston, Massachussetts, MA. August, 2009.
   Paper: [pdf] [bib]
   Slides: [pdf] [www/html] [keynote]
   

   @InProceedings{might2009dependence,
     author =       {Matthew Might and Tarun Prabhu},
     title =        {Interprocedural dependence analysis of higher-order programs via stack reachability},
     booktitle =    {Proceedings of the 2009 {W}orkshop on {S}cheme and {F}unctional {P}rogramming (Scheme 2009)},
     year =         {2009},
     address =      {Boston, Massachussetts, USA},
     month =        {August}
   }
   

7. Matthew Might and Panagiotis Manolios. ``A posteriori soundness for non-deterministic abstract interpretations.'' 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2009). Savannah, Georgia, USA. January, 2009.
   Paper: [pdf] [bib]
   Slides: [pdf] [www/html] [keynote]
   

   @InProceedings{might2009aposteriori,
     author =       {Matthew Might and Panagiotis Manolios},
     title =        {\emph{A posteriori} soundness for non-deterministic abstract interpretations},
     booktitle =    {Proceedings of the 10th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation  ({VMCAI} 2009)},
     year =         {2009},
     address =      {Savannah, Georgia, USA},
     month =        {January}
   }
   

8. Matthew Might. ``Logic-flow analysis of higher-order programs.'' 34th Annual ACM Symposium on the Principles of Programming Languages (POPL 2007). Long paper category. Nice, France. January, 2007. pages 185--198.
   Paper: [pdf] [bib]
   Slides: [pdf]
   

   @InProceedings{might2007lfa,
     author =    {Matthew Might},
     title =     {Logic-Flow Analysis of Higher-Order Programs},
     booktitle = {Proceedings of the 34th {A}nnual {ACM} {S}ymposium on the {P}rinciples of {P}rogramming {L}anguages  ({POPL} 2007)},
     pages =     {185--198},
     year =      {2007},
     address =   {Nice, France},
     month =     {January}
   }
     

9. Matthew Might, Benjamin Chambers and Olin Shivers. ``Model Checking via ΓCFA.'' 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007). Nice, France. January, 2007. pages 59--73.
   Paper: [pdf] [bib]
   

   @InProceedings{might2007gcfamc,
     author =       {Matthew Might and Benjamin Chambers and Olin Shivers},
     title =        {Model Checking via {$\Gamma$CFA}},
     booktitle =    {Proceedings of the 8th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation  ({VMCAI} 2007)},
     pages =        {59--73},
     year =         {2007},
     address =      {Nice, France},
     month =        {January}
   }
   

10. Matthew Might and Olin Shivers. ``Improving flow analyses via ΓCFA: Abstract garbage collection and counting.'' 11th ACM International Conference on Functional Programming (ICFP 2006). Portland, Oregon. September, 2006. pages 13--25.
    Paper: [pdf] [bib]
    Slides: [pdf]
    

    @InProceedings{might2006gcfa,
      author =       {Matthew Might and Olin Shivers},
      title =        {Improving Flow Analyses via {$\Gamma$CFA}: Abstract Garbage Collection and Counting},
      booktitle =    {Proceedings of the 11th {ACM} {I}nternational {C}onference on {F}unctional {P}rogramming  ({ICFP} 2006)},
      pages =        {13--25},
      year =         {2006},
      address =      {Portland, Oregon},
      month =        {September}
    }
    

11. Olin Shivers and Matthew Might. ``Continuations and transducer composition.'' 27th Conference on Programming Language Design and Implementation (PLDI 2006). Ottawa, Canada. pages 295--307. June, 2006.
    Paper: [pdf] [bib]
    Slides: [pdf]
    

    @InProceedings{might2006transducer,
      author =       {Olin Shivers and Matthew Might},
      title =        {Continuations and Transducer Composition},
      booktitle =    {Proceedings of the 27th {C}onference on {P}rogramming {L}anguage {D}esign and {I}mplementation  ({PLDI} 2006)},
      pages =        {295--307},
      year =         {2006},
      address =      {Ottawa, Canada},
      month =        {June}
    }
    

12. Matthew Might and Olin Shivers. ``Environment analysis via ΔCFA.'' 33rd Annual ACM Symposium on the Principles of Programming Languages (POPL 2006). Charleston, South Carolina. January, 2006. pages 127--140.
    Paper: [pdf] [bib]
    Slides: [pdf]
    

    @InProceedings{might2006dcfa,
      author =       {Matthew Might and Olin Shivers},
      title =        {Environment Analysis via {$\Delta$CFA}},
      booktitle =    {Proceedings of the 33rd {A}nnual {ACM} {S}ymposium on the {P}rinciples of {P}rogramming {L}anguages  ({POPL} 2006)},
      pages =        {127--140},
      year =         {2006},
      address =      {Charleston, South Carolina},
      month =        {January}
    }
    

Journal papers

1. Matthew Might and Olin Shivers. ``Exploiting reachability and cardinality in higher-order flow analysis.'' Journal of Functional Programming. Volume 18, Issues 5-6. 2008. pages 821-864.
   Paper: [pdf] [bib]
   

   @Article{might2008exploiting,
     author  = {Matthew Might and Olin Shivers},
     title   = {Exploiting reachability and cardinality in higher-order flow analysis},
     journal = {Journal of Functional Programming},
     year    = {2008},
     volume  = {18},
     number  = {5--6},
     pages   = {821--864}
   }
     

2. Matthew Might and Olin Shivers. ``Analyzing environment structure of higher-order languages using frame strings.'' Journal of Theoretical Computer Science. Volume 375, Issues 1-3. Festschrift for John C. Reynolds's 70th birthday. 2007. pages 137--168.
   Paper: [pdf] [bib]
   

   @Article{might2007dcfa,
     author  = {Matthew Might and Olin Shivers},
     title   = {Analyzing the environment structure of higher-order languages using frame strings},
     journal = {Theoretical {C}omputer {S}cience},
     year    = {2007},
     volume  = {375},
     number  = {1--3},
     pages   = {137--168},
     month   = {May}
   }
     

Dissertation

1. Matthew Might. ``Environment Analysis of Higher-Order Languages.'' Ph.D. Dissertation. Georgia Institute of Technology.
   Paper: [pdf] [bib]
   Slides: [pdf]
   

   @PhdThesis{might2007diss,
     author =       {Matthew Might},
     title =        {Environment Analysis of Higher-Order Languages},
     school =       {Georgia Institute of Technology},
     year =         {2007},
     month =        {June}
   }
   

   
   

Talks and lectures

These are invited talks, lectures or panel discussions; paper-based conference talks are in the papers section.

• "Static analysis of modern software systems: Taming control-flow." Brigham Young University. Provo, Utah. September 10 2009.
  Slides: [pdf] [www/html]
• "Control-flow analysis of higher-order programs." NSF/ACM-sponsored Ph.D. Summer School on Theory and Practice of Language Implementation. Eugene, Oregon. July 23 2009.
  Slides: [pdf] [www/html] [flash]
• "Control-flow analysis of order k (k-CFA)." NSF/ACM-sponsored Ph.D. Summer School on Theory and Practice of Language Implementation. Eugene, Oregon. July 24 2009.
  Slides: [pdf] [www/html] [flash]
• "Efficient control-flow analysis and beyond." NSF/ACM-sponsored Ph.D. Summer School on Theory and Practice of Language Implementation. Eugene, Oregon. July 27 2009.
  Slides: [pdf] [www/html] [flash]
• "Push-down control-flow analysis of higher-order programs." International Conference on Functional Programming Program Committee Workshop. Portland, Oregon. 30 April 2009.
• "The Many-core Fad." Position statement. Cross-cutting systems panel. University of Utah. 30 April 2009.
  Slides: [pdf] [www/html] [www/flash] [keynote]
• "A Brief History of the Freedom of Expressions." Explorations in Computer Science. University of Utah. Fall 2008.
  Slides: [pdf] [www/html] [keynote]

• "Static Analysis of Higher-Order Programs." Given at Max-Planck Institute, Northwestern University, Brandeis University, University of Utah. Spring 2008.
  Slides: [pdf] [www/html] [keynote]

Activities

1. PLDI 2010. Attending. Toronto, Canada. June 2010.
2. Oregon Ph.D. Summer School. Attending. June 15 - 25, 2010.
3. POPL 2011. Workshop Chair. Austin, Texas. January 2011.
4. SAS 2010. Attending. 14-16 September 2010. Perpignan, France.
5. NSAD 2011. Steering Committee Member.

[show past activities]

Teaching

• Fall 2009: Advanced topics in compilation.
• Spring 2009: Programming language analysis.
• Spring 2009: Static analysis seminar.

Blog

blog.might.net is really just a collection of short articles.

Here are the 7 most recent:

Press

1. (New) Twitter plans major move to Salt Lake City. 21 July 2010. Reported by Arrika Von. KSTU. Salt Lake City, Utah. 9:00 PM. [text/video]
2. Is child porn lurking on your computer? 10 November 2009. Reported by Rod Decker. KUTV. Salt Lake City, Utah. 6:00 PM. [text/video]
3. Technology influencing uprising in Iran. 22 June 2009. Reported by John Daley. KSL. Salt Lake City, Utah. 5:00 PM, 6:00 PM. [text/video]

Personal

• Blog.
• Twitter.
• My son's medical blog.
• Amazon wish list.

People

Blogs:

• John Regehr's blog: Embedded in Academia.
• David Van Horn's research weblog.
• Suresh Venkatasubramanian: geomblog.

Co-authors:

• Tarun Prabhu.
• Olin Shivers.
• Yannis Smaragdakis.
• David Van Horn.

Students (that have web pages):

• J.T. Olds.
• Tarun Prabhu.

---

Last modified: Mon Jul 5 18:28:52 MDT 2010