My primary interest is in static analysis of software systems, and static analysis by abstract interpretation in particular. My objective is to build languages, compilers and tools for programmers that improve the security, parallelism and performance of their software.

I run the U Combinator static analysis research group.

Publications

• CiteULike: [my pubs] [my library]

Proceedings papers

1. Matthew Might, Yannis Smaragdakis and David Van Horn. ``Resolving and exploiting the k-CFA paradox: Illuminating functional v. object-oriented program analysis.'' Accepted to Programming Language Design and Implementation 2010 (PLDI 2010). Toronto, Canada. June, 2010. (New)
2. Matthew Might. ``Shape analysis in the absence of pointers and structure.'' Proceedings of the 11th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2010). Madrid, Spain. January, 2010. (New)
   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} 2009)},
     year =         {2010},
     pages =        {263--278},
     address =      {Madrid, Spain},
     month =        {January}
   }
   

3. Matthew Might and Tarun Prabhu. ``Interprocedural dependence analysis of higher-order programs via stack reachability.'' Proceedings of the 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}
   }
   

4. Matthew Might and Panagiotis Manolios. ``A posteriori soundness for non-deterministic abstract interpretations.'' Proceedings of the 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}
   }
   

5. Matthew Might. ``Logic-flow analysis of higher-order programs.'' Proceedings of the 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}
   }
     

6. Matthew Might, Benjamin Chambers and Olin Shivers. ``Model Checking via ΓCFA.'' Proceedings of the 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}
   }
   

7. Matthew Might and Olin Shivers. ``Improving flow analyses via ΓCFA: Abstract garbage collection and counting.'' Proceedings of the 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}
   }
   

8. Olin Shivers and Matthew Might. ``Continuations and transducer composition.'' Proceedings of the 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}
   }
   

9. Matthew Might and Olin Shivers. ``Environment analysis via ΔCFA.'' Proceedings of the 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. SAS 2010. PC Member. Deadline: 19 March 2010.

[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:

• Continuations: Exceptions, back-tracking, generators and coroutines
• Compiling functional languages to C with closure conversion.
• Compiling functional languages directly to Java.
• Fast vector structs with syntax-rules macro-generating macros.
• A functional language for meta-programming in C++ templates.
• Lazy-list-based streams in Scala.
• Learning Scala in small bites.
• Church encodings in Scheme.
• Pattern-matching with derivatives of regular expressions in Scheme.
• Productivity tips for grad students and professors.
• Regular expression matching (by NFA translation) in Java.
• A (side-effecting) denotational interpreter for Lambdo.
• Getting in to grad school.
• An implementation of red-black tree maps in Scala.
• An example of lexing and parsing in Scala using combinators.
• Non-termination without loops, iteration or recursion.
• The Y combinator in Javascript.
• Fermat and Solovay-Strassen implementation in Scheme.
• RSA implementation in Scheme.
• Why infinite (or guaranteed) file compression is impossible.
• HOWTO: Catalog a library with a $10 barcode scanner.
• Tips, tricks and tools for using and learning Unix/Linux.
• Tips, tricks and apps for the iPhone.
• Good programming languages to learn.
• HOWTO: Use Skype for a home phone line.
• Why peer reviewers should use TOR.
• Tips and software for (new) Mac users.
• Preventing and managing repetitive strain injury (RSI).
• Useful books, papers and materials for graduate students.
• Advice for the academic job hunt.

Press

1. Is child porn lurking on your computer? 10 November 2009. Reported by Rod Decker. KUTV. Salt Lake City, Utah. 6:00 PM. [text/video]
2. 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.
• Bertrand's medical blog.
• Amazon wish list.

---

Last modified: Mon Feb 1 10:27:19 MST 2010