Current Software Projects

• Forge: A Tool and Language for Teaching Formal Methods
  Forge is a lightweight formal-methods tool, similar to Alloy 6, built with teaching in mind. Forge provides a progression of sub-languages that gradually build in expressive power to match students' experience and expertise.

(Read about older projects here.)

Publications

• Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
  Ben Greenman, Siddhartha Prasad, Antonio Di Stasio, Shufang Zhu, Giuseppe De Giacomo, Shriram Krishnamurthi, Marco Montali, Tim Nelson, Milda Zizyte
  International Symposium on Formal Methods (FM) 2024
  

• Validation of Formal Models: A Case Study
  Pamela Zave and Tim Nelson
  The Practice of Formal Methods, Essays in Honor of Cliff Jones, Part II
  

• Forge: A Tool and Language for Teaching Formal Methods
  Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney Levine, Julianne Rudner, Ben Ryjikov, Alexander Varga, Andrew Wagner, Luke West, and Shriram Krishnamurthi
  ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (2024)
  

• Conceptual Mutation Testing for Student Programming Misconceptions
  Siddhartha Prasad, Ben Greenman, Tim Nelson, Shriram Krishnamurthi
  The Art, Science, and Engineering of Programming (2024)
  

• Generating Programs Trivially: Student Use of Large Language Models
  Siddhartha Prasad, Ben Greenman, Tim Nelson, Shriram Krishnamurthi
  ACM Conference on Global Computing Education (2023)
  

• Little Tricky Logic: Misconceptions in the Understanding of LTL
  Ben Greenman, Sam Saarinen, Tim Nelson, Shriram Krishnamurthi
  The Art, Science, and Engineering of Programming (2023)
  

• Making Hay from Wheats: A Classsourcing Method to Identify Misconceptions
  Siddhartha Prasad, Ben Greenman, Tim Nelson, John Wrenn, Shriram Krishnamurthi
  Koli Calling International Conference on Computing Education Research (2022)
  

• Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
  Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi
  ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (2022)
  

• Automated, Targeted Testing of Property-Based Testing Predicates
  Tim Nelson, Elijah Rivera, Sam Soucie, Thomas Del Vecchio, John Wrenn, and Shriram Krishnamurthi
  The Art, Science, and Engineering of Programming (2022)
  

• Prototyping Formal Methods Tools: A Protocol Analysis Case Study
  Abigail Siegel, Mia Santomauro, Tristan Dyer, Tim Nelson, and Shriram Krishnamurthi Protocols, Logic, and Strands: Essays Dedicated to Joshua Guttman on the Occasion of his 66.66 Birthday
  

• Solver-Aided Multi-Party Configuration
  Kevin Dackow, Andrew Wagner, Tim Nelson, Shriram Krishnamurthi, and Theophilus A. Benson
  Hot Topics in Networking (HotNets) 2020
  

• Using Relational Problems to Teach Property-Based Testing
  John Wrenn, Tim Nelson, and Shriram Krishnamurthi
  The Art, Science, and Engineering of Programming (2021)
  

• Synthesizing Mutable Configurations: Setting up Systems for Success
  Tim Nelson, Natasha Danas, Theophilos Giannakopoulos, and Shriram Krishnamurthi
  Workshop on Software Engineering for Infrastructure and Configuration Code (SEConfig) 2019
  

• The Human in Formal Methods
  Shriram Krishnamurthi and Tim Nelson
  Formal Methods 2019 (Invited Talk)
  

• CompoSAT: Specification-Guided Coverage for Model Finding
  Sorawee Porncharoenwase, Tim Nelson, and Shriram Krishnamurthi
  Formal Methods 2018
  

• User Studies of Principled Model Finder Output
  Natasha Danas, Tim Nelson, Lane Harrison, Shriram Krishnamurthi, and Daniel J. Dougherty
  Software Engineering and Formal Methods (SEFM) 2017
  

• The Power of "Why" and "Why Not": Enriching Scenario Exploration with Provenance
  Tim Nelson, Natasha Danas, Daniel J. Dougherty, and Shriram Krishnamurthi
  Foundations of Software Engineering (FSE) 2017 (award paper)
  

• Switches are Monitors Too!: Stateful Property Monitoring as a Switch Design Criterion
  Tim Nelson, Nicholas DeMarinis, Timothy Adam Hoff, Rodrigo Fonseca, and Shriram Krishnamurthi
  Hot Topics in Networking (HotNets) 2016
  

• Simon: Scriptable Interactive Monitoring for SDNs
  Tim Nelson, Da Yu, Yiming Li, Rodrigo Fonseca, and Shriram Krishnamurthi
  Symposium on SDN Research (SOSR) 2015
  

• Exodus: Toward Automatic Migration of Enterprise Network Configurations to SDNs
  Tim Nelson, Andrew D. Ferguson, Da Yu, Rodrigo Fonseca, and Shriram Krishnamurthi
  Symposium on SDN Research (SOSR) 2015
  

• Static Differential Program Analysis for Software-Defined Networks
  Tim Nelson, Andrew D. Ferguson and Shriram Krishnamurthi
  International Symposium on Formal Methods (FM) 2015
  

• Tierless Programming and Reasoning for Software-Defined Networks
  Tim Nelson, Andrew D. Ferguson, Michael J. G. Scheer and Shriram Krishnamurthi
  Networked Systems Design and Implementation (NSDI) 2014
  Talk Video (Quicktime)

• Geometric Logic for Policy Analysis
  Salman Saghafi, Tim Nelson and Daniel J. Dougherty
  International Workshop on Automated Reasoning in Security and Software Verification (ARSEC) 2013
  

• A Balance of Power: Expressive, Analyzable Controller Programming
  Tim Nelson, Arjun Guha, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi
  Workshop on Hot Topics in Software Defined Networking (HotSDN) 2013
  

• Aluminum: Principled Scenario Exploration Through Minimality
  Tim Nelson, Salman Saghafi, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
  35th International Conference on Software Engineering (ICSE 2013)
  Download the tool here.
  

• Toward a More Complete Alloy
  Tim Nelson, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
  3rd International Conference on Abstract State Machines, Alloy, B, and Z (ABZ 2012)
  

• The Margrave Tool for Firewall Analysis
  Tim Nelson, Christopher Barratt, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
  24th USENIX Large Installation System Administration Conference (LISA 2010)
  Talk Video (Quicktime)

• On the Finite Model Property in Order-Sorted Logic
  Tim Nelson, Daniel J. Dougherty, Kathi Fisler and Shriram Krishnamurthi
  Synthesis, Verification, and Analysis of Rich Models (SVARM 2010)
  

Technical Reports

• On the Finite Model Property in Order-Sorted Logic
  Tim Nelson, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi
  

Thesis

• First-Order Models for Configuration Analysis
  Tim Nelson
  

Older Software Projects