Formal Methods for Quantitative Program Analysis

My projects tackle problems of knowing what programs will do. These are challenging problems (uncomputable, in fact!). On top of that, we also want to know HOW MANY ways a program can do its thing.

Counting the ways that a program can do something requires analyzing the source code (this is called static analysis), analyzing the running program (this is called dynamic analysis) and performing combinatorial computations (via logic and a field called "model counting"). Doing so allows us to answer questions like "how safe is my code?", "how many test inputs do I need in order to discover some interesting program behavior?", "how complicated is my code?", or “how can an autonomous agent optimize its interaction with my code?”.

 

Relevant background: papers and videos

Application information: In your application, please describe your interest or background in the intersection of mathematics (combinatorics / algebra) and programming languages.

Name of research group, project, or lab
ALPAQA
Why join this research group or lab?

Learn and practice math and programming analysis with other people who also enjoy these topics. 

 

Logistics Information:
Project categories
Computer Science
Mathematics
Algorithms
Human-Computer Interaction
Student ranks applicable
First-year
Sophomore
Junior
Senior
Student qualifications

Excitement about programming languages, program analysis, combinatorics, logic, automated theorem proving, and / or abstract algebra is a real win. With this project you'll emerge with even more of that excitement! Join in! A formal prior background in these areas is possibly beneficial but definitely not necessary--we'll learn together as we go.

Time commitment
Summer - Full Time
Compensation
Paid Research
Number of openings
4
Techniques learned

Program analysis, combinatorics, graph theory, logic, automated theorem proving, abstract algebra, symbolic execution, software development, human-computer interaction. 

Contact Information:
Mentor
Lucas Bang
lbang@hmc.edu
Computer Science Professor
Name of project director or principal investigator
Lucas Bang
Email address of project director or principal investigator
bang@cs.hmc.edu
4 sp. | 40 appl.
Hours per week
Summer - Full Time
Project categories
Algorithms (+3)
Computer ScienceMathematicsAlgorithmsHuman-Computer Interaction