Automated Reasoning Tools and the Formal Verification of
Final Draft of Sunday, December 23, 2007
Deeply surveys the state-of-the-art in the use of automated reasoning tools to prove software programs correct relative to a formal specification of their behavior. It explores the kinds of automated reasoning tools in use today in industry and academia, and the difficulty of developing self-consistent formal specifications of program behavior. The paper includes a discussion of the practical consequences that theoretical limits on computation, like undecidability and NP-completeness, have for formal verification.
|Untitled (the Studio580
Partial Draft of Monday, January 16, 2009
This is a partially completed draft of an academic paper on my Studio580 system. When completed, it will be submitted to journals and conferences. Since I haven’t yet decided precisely where I will submit the paper, each section in this draft is far longer than it needs to be. This is a function of my approach to academic writing—I like to produce a lot more content than I actually need, then winnow the text down. This affords flexibility: in paring down the text, I can pick-and-choose from a range of content to get just what I need to satisfy the interest of a particular conference or publication.
As an individual developer working on research projects, I generally just write brief memos when I need to document development roadmaps, system specifications, and design ideas, instead of spending hours to produce the kind of formal documentation typical of teams working on production projects. Below are three sample memoranda, of various kinds, all related to Studio580 and dated between April and July of 2008.
|Key Abstractions in
the Correction Operation for Hoppe & Lefebvre Texture
Design Memorandum of Monday, April 21, 2008.
Documents the various abstractions used in the multi-scale, pyramidal, progressive-refinement operation (called “correction” by its designers) that lies at the heart of the Hoppe & Lefebvre’s texture synthesis algorithm. The Hoppe & Lefebvre algorithm was developed by Hughes Hoppe and Sylvain Lefebvre at Microsoft Research in 2005. A modified version is used to implement the synthesis engine in Studio580.
Specification for the SynIntegrated Test Applet
Specification Memorandum of Tuesday, June 4, 2008
Serves as an informal requirements specification for SynIntegrated test applet. As I developed Studio580, I produced small “test & debug” applets along the way to serve as test harnesses for various components. SynIntegrated was a test applet that enabled its user to view the texture information being grown by the Studio580’s texture synthesis engine at various intermediate stages of the progressive-refinement algorithm.
|A Design Sketch of a
Strategy for Integrating the Stroke Generation and
Texture Synthesis Modules
Design Memorandum of Friday, July 18, 2008
Describes potential complications that I suspected might develop during the integration of Studio580’s stroke capture and texture synthesis subsystems. Though the subsystems were developed with compatible interfaces, when the time came to roll them together, I thought it best to proceed delicately. This memo is the result of a brainstorming session on problems that might arise during integration, and potential solutions.
Technical Advising & Collaboration
For several years, I have maintained a collaboration with John H. Johnston, a professor of English and Comparative Literature at Emory University in Atlanta. Prof. Johnston’s work explores the evolving intersection between computation and the traditional humane studies, focusing on technologies like artificial life, hyper-real simulation, and new media. I received a substantial acknowledgement in his most recent book, The Allure of Machinic Life: Artificial Life, Cybernetics and the new AI (MIT Press Bradford Series, 2008) for advising on technical details during the book’s production. You can view the book on amazon.com by clicking here.