Dr. Ken Roe

Just me
kendroe@hotmail.com
Computer Science Department
Whiting School of Engineering
The Johns Hopkins University

Who Am I?

I am a staff software engineer at SiFive. My work at SiFive involves 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.

My CV

Talks, Papers and Code

2020

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)