Joseph P. Near

jnear at csail dot mit dot edu

Publications

• Joseph P Near and Daniel Jackson. Rubicon: bounded verification of web applications. In Proceedings of the 20th International Symposium on the Foundations of Software Engineering, 2012. (pdf)

• Joseph P. Near, Aleksandar Milicevic, Eunsuk Kang and Daniel Jackson. A lightweight code analysis and its role in evaluation of a dependability case. In Proceedings of the 33rd International Conference on Software Engineering, 2011.

• Joseph P. Near. An Imperative Extension to Alloy and a Compiler for its Execution. MIT Masters Thesis, 2010. (pdf)

• Joseph P. Near. From Relational Specifications to Logic Programs. In Proceedings of the 26th International Conference on Logic Programming (Technical Communications), 2010. (pdf)

• Joseph P. Near and Daniel Jackson. An Imperative Extension to Alloy. In Proceedings of the 2nd International Conference on Abstract State Machines, Alloy, B and Z, 2010. (pdf)

• Derek Rayside, Zev Benjamin, Rishabh Singh, Joseph P. Near, Aleksandar Milicevic, and Daniel Jackson. Equality and Hashing for (almost) Free: Generating Implementations from Abstraction Functions. In Proceedings of the 31st International Conference on Software Engineering, 2009.

• Joseph P. Near, William E. Byrd, and Daniel P. Friedman. alphaleanTAP: A Declarative Theorem Prover for First-Order Classical Logic. In Proceedings of the 24th International Conference on Logic Programming, 2008. (pdf)

Software

• Rubicon. A domain-specific language and automatic bounded verifier for writing and checking specifications of Ruby on Rails web applications.

• Imperative Alloy. A compiler from the Imperative Alloy language to standard Alloy for analysis by the Alloy Analyzer.

Teaching

• So You've Always Wanted to Learn Haskell? (Instructor; MIT, IAP 2010)

• 6.005. (TA; MIT, Spring 2009)

• C311. (TA; IU, Fall 2005-Spring 2008)