Publications:

2014

  • ICE: A Robust Learning Framework for Synthesizing Invariants
    Pranav Garg, Christof Loeding, P. Madhusudan, and Daniel Neider
    26th Int'l Conf. on Computer Aided Verification, 2014, Vienna, Austria (CAV 2014)
    Paper PDF

  • VAC - Verifier of Administrative Role-based Access Control Policies
    Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen and Gennaro Parlato.
    26th Int'l Conf. on Computer Aided Verification, 2014, Vienna, Austria (CAV 2014)
    Paper PDF

  • Natural Proofs for Data Structure Manipulation in C using Separation Logic
    Edgar Pek, Xiaokang Qiu, P. Madhusudan
    35th ACM SIGPLAN Programming Language Design and Implementation (PLDI 2014)
    Paper PDF

  • Online Learning versus Blended Learning: An Exploratory Study
    Cross, Ashok, Bala, Cutrell, Datha, Kumar, Kumar, Madhusudan, Prakash, Rajamani, Sangameswaran, Sharma, Thies.
    Work in Progress paper, First ACM Conference on Learning at Scale
    Paper PDF

  • 2013

  • Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
    Pranav Garg, P. Madhusudan, and Gennaro Parlato
    20th Static Analysis Symposium (SAS), 2013.
    Paper PDF

  • Learning Universally Quantified Invariants of Linear Data Structures
    Pranav Garg, Christof Loeding, P. Madhusudan, and Daniel Neider
    25th Int'l Conf. on Computer Aided Verification (CAV), 2013.
    Paper PDF

  • Natural Proofs for Structure, Data, and Separation
    Xiaokang Qiu, Pranav Garg, and Andrei Stefanescu, P. Madhusudan
    ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), 2013.
    Paper PDF and Supplementary material

  • Verifying Security Invariants in ExpressOS
    Haohui Mai, Edgar Pek, Hui Xue, Samuel T. King, and P. Madhusudan
    18th Int'l Conf. on Architectural Support for Prog. Lang. and Operating Sys. (ASPLOS), 2013
    PDF

  • Policy Analysis for Self-administrated role-based access control
    Anna Lisa Ferrara, P. Madhusudan, and Gennaro Parlato
    19th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2013
    PDF

  • 2012

  • Predicting Null-Pointer Dereferences in Concurrent Programs
    with Azadeh Farzan , Niloofar Razavi, and Francesco Sorrentino
    20th ACM SIGSOFT Int'l Symp on Foundations of Software Engineering (FSE), 2012.
    PDF

  • Security Analysis of Role-based Access Control through Program Verification
    with Gennaro Parlato and Anna Lisa Ferrara
    25th IEEE Computer Security Foundations Symposium (CSF).
    Harvard University, Cambridge MA, USA, 2012.
    PDF
    See the associated VAC Tool page.

  • Analyzing Temporal Role Based Access Control Models
    with Emre Uzun, Vijay Atluri, Shamik Sural, Jaideep Vaidya, Gennaro Parlato, and Anna Lisa Ferrara
    17th ACM Symposium on Access Control Models and Technologies (SACMAT)
    Newark, USA, 2012.

  • Reachability under Contextual Locking
    with Mahesh Viswanathan and Rohit Chadha
    Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012, Tallinn, Estonia.
    PDF

  • Recursive Proofs for Inductive Tree Data-structures
    with Xiaokang Qiu and Andrei Stefanescu
    Principles of Programming Languages (POPL), 2012, Philadelphia.
    PDF

  • 2011

  • Vetting browser extensions for security vulnerabilities with VEX
    with Sruthi Bandhakavi, Nandit Tiku, Wyatt Pittman, Sam King, and Marianne Winslett
    Research Highlights
    Communications of the ACM (CACM), Vol. 54, Issue 9, September 2011.

  • Synthesizing Reactive Programs
    20th Conference on Computer Science Logic (CSL), Bergen, Norway, 2011.
    PDF

  • Efficient algorithms for deciding properties of heaps using STRAND
    with Xiaokang Qiu
    Static Analysis Symposium (SAS) 2011, Venice, Italy.
    PDF

  • Compositionality entails Sequentializability
    with Pranav Garg
    Int'l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2011.
    PDF

  • Thread Contracts for Safe Parallelism
    with Rajesh Karmani and Brandon Moore
    16th ACM SIGPLAN Annual Symp. on Principles and Practice of Parallel Programming (PPoPP 2011).
    PDF

  • Decidable Logics Combining Heap Structures and Data
    with Gennaro Parlato and Xiaokang Qiu
    ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages (POPL), 2011
    PDF

  • The Tree Width of Auxiliary Storage
    with Gennaro Parlato
    ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages (POPL), 2011
    PDF
    See also Technical Report. that has more proofs.

  • 2010

  • PENELOPE: Weaving Threads to Expose Atomicity Violations
    with Azadeh Farzan and Francesco Sorrentino
    ACM SIGSOFT Int'l Symp. on the Foundations of Software Engineering (FSE), Santa Fe, New Mexico, USA, November 2010.
    PDF

  • VEX: Vetting Browser Extensions For Security Vulnerabilities
    with Sruthi Bandhakavi, Sam King, and Marianne Winslett
    Proc. of USENIX Security Symposium. Washington D.C, USA, August 2010.
    *** Best paper award ***
    See the VEX Website for details on the tool.
    PDF

  • Model-checking Parameterized Concurrent Programs using Linear Interfaces
    with Salvatore La Torre and Gennaro Parlato
    To appear in 22nd Int'l Conf. on Computer Aided Verification (CAV), 2010, Edinburgh, UK.
    PDF

  • The language theory of bounded context-switching
    with Salvatore La Torre and Gennaro Parlato
    9th Latin American Theoretical Informatics Symposium (LATIN), Oaxaca, Mexico, 2010.
    PDF.

  • 2009

  • Query automata for nested words
    with Mahesh Viswanathan
    34th International Symposium on Mathematical Foundations of Computer Science (MFCS), High Tatras, Slovakia, 2009.
    PDF.

  • Meta-analysis for Atomicity Violations under Nested Locking
    with Azadeh Farzan and Francesco Sorrentino
    Computer Aided Verification (CAV), Grenoble, France, 2009.
    PDF.

  • Reducing Context-bounded Concurrent Reachability to Sequential Reachability
    with Salvatore La Torre and Gennaro Parlato
    Computer Aided Verification (CAV), Grenoble, France, 2009.
    PDF.

  • Analyzing Recursive Programs using a Fixed-point Calculus
    with Salvatore La Torre and Gennaro Parlato
    ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI)
    Dublin, Ireland, 2009.
    PDF.
    See also the Getafix page for the tool and experiments

  • The Complexity of Predicting Atomicity Violations
    with Azadeh Farzan
    Int'l Conf. on Tools and Algorithms for the Construction & Analysis of Systems (TACAS)
    York, UK, 2009.
    PDF.
    Slides: Powerpoint, PDF

  • Adding nesting structure to words.
    with R. Alur
    Journal of the ACM (JACM), Vol. 56(3), pages 1-43, ACM, 2009.
    PDF.

  • CANDID: Dynamic Candidate Evaluations for Automatic Prevention of SQL Injection Attacks
    with Prithvi Bisht and V.N. Venkatakrishnan.
    ACM Transactions on Information and System Security (TISSEC), 2009.
    PDF.

  • 2008

  • Parallel Computing at Illinois: The UPCRC Agenda
    with S. Adve, V. Adve, G. Agha, M.I. Frank, M.J. Garzaran, J.H.Hart, W.W. Hwu, R.E. Johnson, L.V. Kale, R. Kumar, D. Marinov, K. Nahrstedt, D. Padua, S. Patel, G. Rosu, D. Roth, M.Snir, J. Torrellas, C. Zilles
    Whitepaper PDF.

  • A Formal Framework for Reflective Database Access Control Policies
    with Lars Olson and Carl Gunter.
    15th ACM Conference on Computer and Communications Security (CCS)
    Alexandria, USA, 2008.
    PDF.

  • An Infinite Automaton Characterization of Double Exponential Time
    with Gennaro Parlato and Salvatore La Torre.
    17th EACSL Annual Conference on Computer Science Logic
    Bertinoro, Italy, 2008.
    Conference version, More complete version with an appendix

  • Monitoring Atomicity in Concurrent Programs
    with Azadeh Farzan
    Computer Aided Verification (CAV), Princeton, USA, 2008.
    PDF.

  • Context-Bounded Analysis of Concurrent Queue Systems
    with Gennaro Parlato and Salvatore La Torre.
    Tools and Algorithms for the Construction and Analysis of Systems
    (TACAS), Budapest, Hungary, 2008.
    PDF.

  • 2007

  • CANDID: Preventing SQL Injection Attacks using Dynamic Candidate Evaluations
    with Sruthi Bandhakavi, Prithvi Bisht and V.N. Venkatakrishnan.
    14th ACM Conference on Computer and Communications Security (CCS)
    Alexandria, USA, 2007.
    PDF.

  • A Robust Class of Context-Sensitive Languages
    with Gennaro Parlato and Salvatore La Torre.
    22nd IEEE Symp. on Logic in Computer Science (LICS)
    Wroclaw, Poland, 2007.
    PDF.

  • Visibly Pushdown Automata for Streaming XML
    with Viraj Kumar and Mahesh Viswanathan.
    Int'l World Wide Web Conference (WWW)
    Alberta, Canada, 2007.
    PDF.

  • Causal Dataflow Analysis for Concurrent Programs
    with Azadeh Farzan.
    Tools and Algorithms for the Construction and Analysis of Systems
    (TACAS), Braga, Portugal, 2007.
    PDF.

  • 2006

  • Minimization, Learning, and Conformance Testing of Boolean Programs
    with Viraj Kumar and Mahesh Viswanathan.
    Int'l Conf on Concurrency Theory (CONCUR), Bonn, Germany, 2006.
    PDF.

  • Causal Atomicity
    with Azadeh Farzan.
    Computer Aided Verification (CAV), Seattle, USA, 2006.
    PDF.

  • Languages of nested trees
    with Rajeev Alur and Swarat Chaudhuri.
    Computer Aided Verification (CAV), Seattle, USA, 2006.
    PDF.

  • Adding Nesting Structure to Words
    with Rajeev Alur.
    Developments in Language Theory (DLT), Santa Barbara, USA, 2006.
    PDF.

  • Modular Strategies for Recursive Game Graphs
    with Rajeev Alur and Salvatore La Torre.
    Theoretical Computer Science, Special Issue for TACAS 2003
    Volume 354, Issue 2, 28 March 2006, Pages 230-249.
    PDF; Link to journal article

  • A Fixpoint Calculus for Local and Global Program Flows
    with Rajeev Alur and Swarat Chaudhuri.
    Principles of Programming Languages (POPL), Charleston, USA, 2006.
    Postscript, PDF.

  • 2005

  • The MSO Theory of Connectedly Communicating Processes
    with Yang Shaofa and P.S. Thiagarajan.
    Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2005
    Postscript, PDF.

  • Congruences for visibly pushdown languages
    with Rajeev Alur, Viraj Kumar and Mahesh Viswanathan.
    Int'l Coll. on Automata, Lang. and Prog. (ICALP), Lisboa, Portugal, 2005.
    Postscript, PDF.

  • Symbolic Compositional Verification by Learning Assumptions
    with Rajeev Alur and Wonhong Nam.
    Computer Aided Verification (CAV), Edinburgh, UK, 2005.
    Postscript, PDF.

  • Symbolic Computational Techniques for Solving Games
    with Rajeev Alur and Wonhong Nam.
    Journal version of BMC'03 paper,
    International Journal on Software Tools for Technology Transfer (STTT)
    February, 2005, © Springer-Verlag
    Postscript of prelim version, Paper on Springer's site

  • On-the-fly reachability and cycle detection for recursive state machines
    with Rajeev Alur, Swarat Chaudhuri, and Kousha Etessami.
    TACAS '05, April 4-8, Edinburgh, UK.
    Postscript

  • Perturbed timed automata
    with Rajeev Alur and Salvatore La Torre.
    Hybrid Systems: Computation and Control (HSCC),
    Zurich, Switzerland, 2005.
    Postscript, PDF

  • Synthesis of Interface Specifications for Java Classes
    (Version 2, July 2004: See the JIST page)
    with Rajeev Alur, Pavol Cerny and Wonhong Nam.
    32nd ACM SIGPLAN-SIGACT Symp. on Principles of Prog. Languages,
    POPL'05, Long Beach, California, USA, Jan 2005.
    Postscript, PDF

  • 2004

  • Visibly pushdown games
    with Christof Loeding and Olivier Serre.
    Foundations of Software Tech. and Theoretical Comp. Sc. (FSTTCS),
    Chennai, India, 2004.
    Postscript

  • Decision problems for timed automata: A Survey
    with Rajeev Alur
    4th Int'l School Formal Methods for the design of
    computer, communication and software systems: Real Time (SFM-04:RT),
    Bertinoro, Italy, 2004. LNCS © Springer-Verlag
    Postscript

  • Optimal Reachability for Weighted Timed Games
    with Rajeev Alur and Mikhail Bernadsky.
    ICALP, 31st Int'l Colloquium on Automata, Languages and Programming,
    Turku, Finland, 2004. LNCS © Springer-Verlag
    Abstract, PDF

  • Visibly pushdown languages
    with Rajeev Alur.
    STOC, Symp. on Theory of Computing, Chicago, USA, 2004.
    Abstract, PDF

  • A Temporal Logic for Nested Calls and Returns
    with Rajeev Alur and K. Etessami.
    TACAS, Barcelona, Spain, 2004. LNCS © Springer-Verlag
    Abstract, Postscript

  • 2003

  • Playing Games with Boxes and Diamonds
    with Rajeev Alur and Salvatore La Torre.
    CONCUR, Marseilles, France, 2003, LNCS © Springer-Verlag
    Abstract, Postscript

  • Symbolic Computational Techniques for Solving Games
    with Rajeev Alur and Wonhong Nam.
    Bounded Model Checking Workshop, Boulder, Colorado, USA, 2003,
    Electronic Notes in Theoretical Computer Science, Vol 89, Issue 4.
    Abstract, Postscript, PDF

  • Modular Strategies for Infinite Games on Recursive Graphs
    with Rajeev Alur and Salvatore La Torre.
    CAV, Boulder, Colorado, USA, 2003, LNCS © Springer-Verlag
    Abstract, Postscript

  • Timed Control with Partial Observability
    with Deepak D'Souza, Patricia Bouyer and Antoine Petit.
    CAV, Boulder, Colorado, USA, 2003, LNCS © Springer-Verlag
    Abstract, Postscript

  • Model-checking Trace Event Structures
    LICS, Ottawa, Canada, 2003, © IEEE
    Abstract, Postscript

  • Modular Strategies for Recursive Game Graphs
    with Rajeev Alur and Salvatore La Torre.
    9th TACAS, Warsaw, Poland, 2003, LNCS © Springer-Verlag
    Abstract, Postscript

  • 2002

  • Dynamic Message Sequence Charts
    with Martin Leucker and Supratik Mukhopadhyay.
    22nd FSTTCS, Kanpur, India, 2002, LNCS © Springer-Verlag
    Abstract, Postscript

  • A Decidable Class of Asynchronous Distributed Controllers
    with P.S. Thiagarajan.
    CONCUR, Brno, Czech Republic, 2002, LNCS 2421 © Springer-Verlag
    Abstract, Postscript

  • Timed Control Synthesis for External Specifications
    with Deepak D'Souza, CMI.
    STACS, Antibes - Juan les Pins, France, 2002,
    LNCS 2285 © Springer-Verlag
    Abstract, Postscript

  • Branching-time controllers for discrete event systems
    with P.S. Thiagarajan, CMI.
    CONCUR '98 Special Issue, Theoretical Computer Science,
    274 1-2 (2002) © Elsevier Sceince
    Abstract, Postscript, PDF (actual journal version)

  • 2001

  • Control and Synthesis of Open Reactive Systems
    Ph.D. thesis, November 2001
    Abstract, Postscript

  • Beyond Message Sequence Graphs
    with B. Meenakshi.
    21st FSTTCS, Bangalore, India, 2001, LNCS 2245 © Springer-Verlag
    Abstract, Postscript

  • Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs
    28th ICALP, Crete, Greece, 2001, LNCS 2076 © Springer-Verlag
    Abstract, Postscript

  • Distributed Controller Synthesis for Local Specifications
    with P.S. Thiagarajan.
    28th ICALP, Crete, Greece, 2001, LNCS 2076 © Springer-Verlag
    Abstract, Postscript

  • Before 2000

  • Open systems in reactive environments: Control and Synthesis
    with Orna Kupferman, P.S. Thiagarajan, Moshe Vardi.
    11th CONCUR, Penn. State Univ., USA, 2000, LNCS 1877 © Springer-Verlag
    Abstract, Postscript

  • Controllers for discrete event systems via morphisms
    with P.S. Thiagarajan, CMI.
    9th CONCUR, Nice, France, 1998, LNCS 1466 © Springer-Verlag
    Abstract, Postscript

  • On-the-fly verification of Product-LTL
    with Deepak D'Souza, CMI.
    National Seminar on Theoretical Computer Science, Madras, June '97.
    Abstract, Postscript

  • An on-the-fly algorithm for linear-time temporal logic
    M.Sc. thesis, 1994
    Abstract, Postscript