Me :^)

Dan DaCosta


University of Minnesota (Ph. D.)

Degree Doctor of Philosophy in Computer Science (in progress)
Advisor Dr. Gopalan Nadathur
Thesis Reasoning about Linear Logic Specifications (working title)
Time Frame 2011 — 2017

Drexel University (M.S.C.S.)

Degree Master of Science in Computer Science
Advisor Dr. Spiros Mancoridis
Thesis pcapstich: A Tool to Collect Singleton One-way Delay and Loss Measurements
Time Frame 2002 — 2011

Drexel University (B.S.C.S.)

Degree Bachelor of Science in Computer Science
Time Frame 1998 — 2002


Rockwell Collins

Title Ph.D. Intern
Time Frame 2013 — present

Formal Software Verification (2015-present)

AutoCorress is an extension to the Isabelle Theorem Prover that encodes a large subset of the C programming language into a monadic form better suited for human reasoning, i.e., it closely resembles the original code. My task is to understand how to effectively use AutoCorress to verify relevant properties relating to Rockwell Collins work on the SMACCMS project.

Automated System Requirement Verification (2013-2015)

Primary developer of SpeAR, a tool for system requirement specification and verification. SpeAR accepts formalized requirements and translated these requirements to a synchronous dataflow language. Another tool, jkind, translated this synchronous dataflow language to specifications suitable for SMT solvers. Through this series of translation, some properties of the specified system requirements could be verified in an automated fashion. SpeAR is written in Java using the Eclipse IDE with the xtext plugin.

Lockheed Martin

Title Senior Member of the Engineering Staff
Time Frame 2003 — 2011

Malware Provenance (2010 — 2011)

Applied statistical modeling techniques to data retrieved via analysis of binary malware in an attempt to recover authorship information.

Transparent Protocol Layer Altering Network Device (2005 — 2010)

Worked with team members in the Advanced Technology Laboratory to design and implement a network device that could alter standard protocol behaviors to better suit network characteristics. The modifications to protocol behavior were implemented such that clients required no modification or non-standard configuration. The system allowed for easy modification of protocol behavior through configuration files and served as an experiment platform for new protocol modifications. The device was tested during a number of live aerial exercises. Later revisions of this project relied extensively on the Click Modular Router.

Buffer Overflow Mitigation (2003 — 2004)

Developed an experimental technique and framework that allowed buffer overflows to be detected and mitigated in c code at runtime. The prototype framework for this technique used the C Intermediate Language to transform programs into ones that would dynamically increase buffer size upon detection of overruns. Buffer overruns were detected using electric fence.


University of Minnesota

Title Teaching Assistant
Time Frame 2011 — 2015

Advanced Programming Principles Principles (x3)

Students were introduced to techniques for creating correct, robust, modular programs including: computing with symbolic data, recursion/induction, functional programming, impact of evaluation strategies, organizing data/computations around types, search-based programming, informal reasoning about programs.

Program Design and Development (x3)

A project based course intended to expose students to: principles of programming design/analysis, concepts in software development, large development using C/C++, data structures, debugging, files, I/O, state machines, testing, and coding standards.

Programming Languages (x2)

This course had two primary goals: (1) to expose students to language design principles, concepts, constructs; (2) to make students more familiar with language paradigms and their applications.



  • Dan DaCosta and Gopalan Nadathur. Towards Reasoning about Properties of Imperative Programs using Linear Logic. Midwest Verification Days 2014, Columbia, MO, October 3-4, 2014.

  • Jesse Brown and Daniel DaCosta. Synthesizing Adaptive Protocols by Selective Enumeration (SYNAPSE). Symposium on Click Modular Router, Belgium, November 23-24, 2009.

  • Dan DaCosta and Todd Hughes. Adaptive Code Injection Attack Mitigation. Sante Fe Institute Business Network Topical Meeting - Adaptive and Resilent Computing Security (ARCS), November 3rd and 4th 2004, Sante Fe, New Mexico.

Technical Skills

Programming Languages OCaml, Python, C, Java, Teyjus, C++, Perl, Haskell
Verification Tools Isabelle, AutoCorres, Abella, jkind, Coq
General Development Tools Emacs, GDB, Valgrind, Eclipse, Vim, Xtext, SQLite
Web Development Tools Pyramid, Jekyll, Ziggurat Foundations