Professor of Computer Science at Stevens Institute of Technology. Here's contact info and Curriculum Vitae.
Spring 2019 -- Formal Modeling and Analysis for Software Security
Fall 2018 -- Introduction to Computer Science; and Formal Verification of Software
Fall 2017 -- on sabbatical as Visiting Fellow at Princeton University, in the DeepSpec project
Spring 2017 -- Introduction to Computer Science Honors II
Fall 2016 -- Formal Modeling and Analysis for Software Security; and Societal Impact of Information Technologies
Spring 2016 -- Introduction to Computer Science Honors II
Fall 2015 -- Introduction to Computer Science; and Discrete Structures
Spring 2015 -- Principles of Programming Languages
For undergrad and MS students: Scholarships for Service.
Undergraduate summer research: Contact me early in Spring semester for projects, supported by NSF and the Stevens Scholars program.
PhD positions: From time to time I take on new PhD students for research on secure information flow in software: policies, static analysis, and runtime monitoring for Android and other platforms. Full funding is provided. The ideal candidates have background in programming language theory and implementation or formal methods.
Affiliated with: CASSIA, the Center for the Advancement of Secure Systems and Information Assurance; also the DeepSpec project.
Postdoctoral research associates:
Minh Ngo -- working on Relational Verification for Information Assurance and Privacy,
NSF award SaTC CNS-1718713.
Mounir Assaf (2015-17) working on Hyperproperty Abstraction for Information Flow Control funded by NSF EAGER award CCF-1649884.
Current and past PhD students: Ramana Nagasamudram; Mohammad Nikouei; Andrey Chudnov (finished Spring 2016); Chunyu Tang (finished Fall 2013); Stan Rosenberg (finished Summer 2011); Qi Sun (finished Fall 2007).
I'm working on Relational Verification for Information Assurance and Privacy (NSF award SaTC CNS-1718713).
I worked with Anindya Banerjee (IMDEA Software), Gary Leavens (U. Central FL.), and others on Flexible and Practical Information Flow Assurance for Mobile Apps
(NSF award 1228930) --see the
With support from DHS I worked on Tunable Information Flow with researchers at HRL Laboratories.
I work with Gary Leavens and others on the Java Modeling Language (JML), and with Leila Silva (UFS Brazil), Giovanny Lucero (UFS Brazil), and Augusto Sampaio (UFPE Brazil) on refactoring (NSF awards CNS-0708330 and CCF-0915611).
With support from Microsoft Research I worked with Andy Gordon and François Dupressoir on verifying cryptographic code in C, and collaborated on the Spec#/Boogie software specification/verification project.
With support from NSF I worked with Anindya Banerjee on Access Control and Downgrading in Information Flow Assurance, collaborating with Tamara Rezk and Gilles Barthe (INRIA), Marco Pistoia (IBM), Qi Sun and Stan Rosenberg. See our Secure Information Flow Inferencer and Verifier for Region Logic.
With support from Telcordia and the U.S. Government I worked with Susanne Wetzel and Chunyu Tang on high assurance for security in wireless networking.
I co-chaired (with Rohit Gheyi) the 15th
Brazilian Symposium on Formal Methods.
I co-chaired (with Stephen Chong) the 4th ACM SIGPLAN Workshop on
Programming Languages and Analysis for Security associated with
PLDI 2009 in Dublin.
I co-chaired (with Peter O'Hearn) the 2008 Theory Workshop of
the Second IFIP Working Conference on
Verified Software: Theories, Tools, Experiments and I co-chaired the
I chaired the Theory Panel of the
Verified Software Initiative and am a Corresponding Member of the
Verified Software Repository Network.
Editorial Boards: Formal Aspects of Computing and The Journal of Object Technology.
The timeliness of my stylish home page, Freedom to Tinker, Empowering Underrepresented Groups in Technology, speed limits for chumps, my guitar teacher, verifying what counts, air quality, life above 20 kHz, my Capoeira Angola master, quanta, the African diaspora, my Smyrneika and voice teachers shaking away like a rattlesnake, pop record ageing fan, Pandora's locked box, the desk upon which it stands, the cry of the imaginary cuica.