Joseph P. Near

jnear at csail dot mit dot edu


  • Joseph P. Near and Daniel Jackson. Derailer: Interactive Security Analysis for Web Applications. To appear in Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2014. (pdf)

  • Emina Torlak, Mana Taghdiri, Greg Dennis, and Joseph P. Near. Applications and extensions of Alloy: past, present and future. In Mathematical Structures in Computer Science, volume 23 number 4, 2013.

  • 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 (FSE), 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 (ICSE), 2011.

  • 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)

  • William E. Byrd, Daniel P. Friedman, Ramana Kumar, and Joseph P. Near. A Shallow Scheme Embedding of Bottom-Avoiding Streams. To appear in a special issue of Higher-Order and Symbolic Computation, in honor of Mitchell Wand's 60th birthday. (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)

Technical Reports

  • Joseph P. Near and Daniel Jackson. Symbolic execution for (almost) free: Hijacking an existing implementation to perform symbolic execution. Technical Report MIT-CSAIL-TR-2014-007, Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge, Massachusetts, April 2014. (pdf)


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


  • Derailer. A visualization-guided static analysis for finding security bugs in Ruby on Rails applications.

  • 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.


Room 32-G708
MIT Computer Science and Artificial Intelligence Lab
32 Vassar St.
Cambridge, MA 02139

Last modified: Jul 26 07:55:27 EST 2014