My main research interest lies in formal methods and verification. I enjoy working with the mathematics behind programming languages, more specifically functional languages. My current work uses abstract interpretation to help verify the transformation of specifications between various modeling domains.

Systems today have become so complex it's difficult to verify that as a whole they will work correctly. Abstract interpretation allows the ability to push away unneeded information and focus on a specific problem. Using the Galois connection along with abstract interpretation it's possible to prove that by pushing away this unneeded information you neither gain nor lose precision. This allows large systems to be broken into smaller pieces, verified, and put back together knowing that they will still function as desired.

I'm currently working towards my PhD in Computer Science under the direction of Dr. Perry Alexander at The University of Kansas in Lawrence, KS, USA. Dr. Alexander's system-level design language, Rosetta, serves as the basis for my research.

2007

Streb, J. and P. Alexander, "A Lattice of Coalgebras for Aspect-Oriented Modeling" submitted to Early Aspects at ICSE: Workshop in Aspect-Oriented Requirements Engineering and Architecture Design , Minneapolis, MN, May 21, 2007

2006

Streb, J., G. Kimmell, N. Frisby, P. Alexander, "Domain Specific Model Composition Using A Lattice Of Coalgebras" submitted to OOPSLA Workshop on Domain Specific Modeling, Portland, OR, October 22, 2006.

Streb, J. and P. Alexander, "Using a Lattice of Coalgebras For Heterogeneous Model Composition" submitted to MoDELS Workshop on Multi-Paradigm Modeling, Genova, Italy, October 3, 2006.

To help learn the functional programming language, Haskell, I created a language for representing dance choreography using it. Three different versions exist, each a little more in depth than the previous. I've defined new data structures for representing the five basic positions of dance, functions for changing dance positions, as well as a parser, type checker, evaluator, and pretty printer. I've also used the catamorphism and monads to carry the current state of a dancer around. Since this was used as a learning tool only, the versions may not be fully functional.