# Dr. Ken Roe

## Who Am I?

I now work at Intel doing formal verification of microprocessors.
I recently worked at SiFive
using the Coq theorem prover to develop a formally verified CPU. I hold
a PhD in Computer Science from Johns Hopkins.
I defended my thesis titled
"Toward a tool to verify complex data structure invariants" on Feb 15, 2018.
I returned to graduate school after working in Silicon
Valley for many years. Many of the ideas developed in my thesis came
out of my experiences in the industry. I have now returned to Silicon Valley
to turn my research into practice. Check out my LinkedIn profile
here.

## Research

I am developing a static analysis tool for C programs. My initial goal
is to build a tool that can eliminate many common memory allocation
errors. Eventually, I would like to address many complex types of
errors including those that arise from complex intricate interactions
between data structures. A few years ago,
I developed an SMT prover. See the talks and papers below for more
details.
My advisor is
Scott Smith

## Side projects

I am an avid mobile developer. Check out the folowing web site for
more information:
http://www.roemobiledevelopment.com.
If you are thinking of getting into iPhone development, I will warn that
you will most likely not get rich from it. I do get a fairly steady income
from my apps. However, I could make more money working at a job.

## Talks, Papers and Code

### 2020

Hardware Verification talk given at Intel and Sandia National Lab

Check out the Kami language and the ProcKami formally verified processor that I am helping to develop at SiFive
here.

Feature engineering with clinical expert knowledge: A case study assessment of machine learning model complexity and performance

### 2018

NECHS 2018 abstract

Slides from my defense

My dissertation (PDFA version)

GITHUB repository for both CoqPIE and PEDANTIC (Runs on a Mac with Coq 8.5 installed)

GITHUB repository for my Coq rewriting library (Runs on a Mac with Coq 8.7 installed)

### 2017

A paper submitted to CPP 2018 describing the advanced rewriting library

A Poster I presented on biomedical data analysis (August)

A paper on PEDANTIC at MEMOCODE2017

The accompanying poster at MEMOCODE2017

My talk at MEMOCODE2017

A poster presented at PLDI 2017

### 2016

HCSS 2016 poster

A COQPIE paper accepted at ITP2016

My talk at ITP2016

### 2015

A Poster for POPL 2015

A Talk given at UCSD and Kestrel in June 2015

HCSS 2015 poster

A paper on functional reactive programming presented at SPLASH-E 2015

### 2014

A Paper I submitted to PADL 2014.

A poster presented at HCSS 2014

### 2013

A paper I submitted to ITP2013.

A Coq model that goes along with the ITP2013 paper.

A Poster I presented for the 2013 SRC at PLDI.

My GBO statement (Sept 2013).

My GBO slides (Sept 2013).

### 2012

#### XSS attack game resources

Presentation

Web site

### 2011

A paper I submitted to ITP2011.

A Coq model that goes along with the ITP2011 paper.

### 2010

A Talk I gave at IBM.

### 2006

My CAV'06 talk

My CAV'06 paper on The Heuristic Theorem Prover The Heuristic Theorem Prover: Yet another SMT Modulo Theorem Prover (Tool Paper)