Publications

(by subject)

• Program Analysis

  • Scalable Flow-Sensitive Pointer Analysis for Java with Strong Updates
    (with Arnab De),
    in proc. ECOOP 2012, LNCS 7313.

  • Dataflow analysis for data-race free programs,
    (with Arnab De and Rupesh Nasre),
    in Proc. ESOP 2011, LNCS 6602, 2011.

• Timed automata

  • Equivalence of the Pointwise and Continuous Semantics of First Order Logic with Linear Constraints
    (with Raveendra Holla and Raj Mohan M)
    (manuscript).

  • Conflict-Tolerant Hybrid Controllers. (with Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath) (to appear in Journal of IISc, 2013).

  • Conflict-Tolerant Real-Time Specifications in Metric Temporal Logic
    (with Sumesh Divakaran and Raj Mohan M.), Technical Report.

  • Deepak D'Souza, Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath: Supervisory control for real-time systems based on conflict-tolerant controllers, in Proc. 5th IEEE Conf. on Automation Science and Engineering (CASE) 2009.

  • Conflict-Tolerant Real-Time Features
    (with Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath)
    in 5th Int. Conference on the Quantitative Evaluation of Systems (QEST 2008), 14-17 September 2008, Saint-Malo, France, pages 274-283.

  • Eliminating past operators in Metric Temporal Logic
    (with Raj Mohan M and Pavithra Prabhakar)
    in Perspectives in Concurrency, Universities Press, 2008, pages 86--106.

  • Automata and logics for finitely varying functions
    (with Fabrice Chevalier, Raj Mohan M, and Pavithra Prabhakar)
    in Annals of Pure and Applied Logic, Volume 161, Issue 3, December 2009, Pages 324-336. (Definitive version.) An extended version will also appear as the article Automata and Logics over signals in the review volume "Modern Applications of Automata Theory", IISc-World Scientific Press, 2010.

  • Counter-free input-determined timed automata
    (with Fabrice Chevalier and Pavithra Prabhakar),
    in FORMATS 2007, LNCS 4763, pp. 82--97. A Technical Report is also available.

  • On the expressiveness of TPTL in the pointwise and continuous semantics
    (with Raveendra Holla and Deepak Vankadaru)
    (manuscript).

  • On continuous timed automata with input-determined guards
    (with Fabrice Chevalier and Pavithra Prabhakar)
    in Proc. FSTTCS 2006, LNCS vol. 4337, pp. 369-380 (2006).

  • On the expressiveness of MTL with past operators
    (with Pavithra Prabhakar)
    in Proc. FORMATS 2006, LNCS 4202, pp. 322-336 (2006).

  • Eventual timed automata
    (with M. Raj Mohan)
    FSTTCS 2005, Springer LNCS 3821, 322--344 (2005). Also available as Technical Report.

  • On the expressiveness of MTL in the pointwise and continuous semantics
    (with Pavithra Prabhakar)
    in Formal Methods Letters (Software Tools for Technology Transfer), Vol. 9, No. 1, pp 1--4, Springer (2007). Also available as a Technical Report.

  • Fault diagnosis using timed automata
    (with Patricia Bouyer and Fabrice Chevalier)
    in Proc. FOSSACS 2005, LNCS 3441, pp. 219--233.

  • On timed automata with input-determined guards
    (with Nicolas Tabareau),
    in Proc. FORMATS-FTRTFT 2004, LNCS 3253 (2004).
  • A Logical Characterisation of Event Clock Automata
    in Intl. Journal of Foundations of Computer Science, Vol. 14, No. 4, World Scientific (2003), 625--639.

  Preliminary version in A Logical Characterisation of Event Recording Automata
  Proc. FTRTFT 2000, LNCS 1926, 2000.

  • Product Interval Automata,
    (with P.S.Thiagarajan)
    in Sadhana, Academy Proceedings in Engineering Sciences, Vol. 27, No. 2, Indian Academy of Sciences (2002), 181--208.

    Preliminary version in Product Interval Automata: A Subclass of Timed Automata
    (with P. S. Thiagarajan)
    Proceedings of 19th FSTTCS, LNCS 1732, 1999.

  • A Logical Study of Distributed Timed Automata
    Ph.D. Thesis submitted to BITS, Pilani, 2000.

• Automated controller synthesis

  • Fault diagnosis using timed automata
    (with Patricia Bouyer and Fabrice Chevalier)
    in Proc. FOSSACS 2005.

  • Timed control with partial observability
    (with Patricia Bouyer, P. Madhusudan, and Antoine Petit),
    in Proc. 15th Conf. on Computer Aided Verification (CAV 2003), LNCS 2725 (2003).
  • Timed control synthesis for external specifications
    (with P. Madhusudan)
    Proc. STACS 2002, LNCS 2285, 2002.

• Temporal Logics

  • A compositional hierarchical monitoring automaton construction for LTL,
    (with Raj Mohan M.),
    in proc. ICTAC 2012, LNCS vol. 7521.

  • Conflict-Tolerant Specifications in Temporal Logic
    (with Sumesh Divakaran and Raj Mohan M.), in proc. India Software Engineering Conference (ISEC) 2010.
    Technical Report

  • A decidable temporal logic of repeating values
    (with Stephane Demri and Regis Gascon)
    in Proc. Symposium on Logical Foundations of Computer Science (LFCS) 2007, LNCS 4514, pp. 180--194.

    Journal version in: Temporal Logics of Repeating Values (with Stéphane Demri and Régis Gascon),
    Journal of Logic and Computation, Volume 22, Issue 5, Pp. 1059-1096 (2012).

  • An Automata-Theoretic Approach to Constraint LTL,
    (with Stéphane Demri)
    in Proc. 22nd Foundations of Software Technology and Theoretical Computer Science (FSTTCS) LNCS 2256 (2002).

    Journal version in Information and Computation, Vol. 205, issue 3, pp 380--415.

  • On-the-fly Verification for Product-LTL
    (with P. Madhusudan)
    Proceedings of Seventh National Seminar on Theoretical Computer Science, 1997.
  • On-the-fly Verification for Linear Time Temporal Logic
    M.Phil. Dissertation submitted to BITS, Pilani, 1997.

• Verification of Security Properties

  • Model-checking bisimulation-based information flow properties for infinite state systems,
    (with Raghavendra K. R.),
    in proc. ESORICS, LNCS vol. 7459 (2012).

  • On the Decidability of Model-Checking Information Flow Properties
    (with Raveendra Holla, Janardhan Kulkarni, Raghavendra K. Ramesh, Barbara Sprick)
    in ICISS 2008, Hyderabad, pages 26-40.

  • Checking unwinding conditions for finite state systems
    (with K. R. Raghavendra)
    To appear in Proc. VERIFY 2006 (2006).

  • A unification-based decision procedure for cryptographic protocol analysis
    (with Deepak Bhardwaj)
    WITS 2006 (2006).

  • An automata-based approach to verifying information flow properties
    (with K R Raghavendra and Barbara Sprick)
    in Proc. ARSPA Workshop 2005, ENTCS vol 135, issue 1 (2005).

• Formal Methods in Software Engineering

  • Analysing Message Sequence Graph Specifications
    (with Joy Chakraborty and K. Narayan Kumar)
    Technical Report.

  • Java Memory Model aware Software Validation
    (with Arnab De and Abhik Roychoudhury)
    in PASTE'08 Workshop.

  • Conflict-Tolerant Features
    (with Madhu Gopinathan)
    in proc. 20th Int. Conference on Computer Aided Verification (CAV) 2008, Princeton, pages 227-239. Technical Report.

  • Computing complete test graphs for hierarchical systems
    (with Madhu Gopinathan)
    in Proc. IEEE SEFM 2006, pp. 70-79 (2006).

  • Checking consistency of SDL+MSC specifications
    (with Madhavan Mukund),
    in Proc. 10th International SPIN Workshop on Model Checking of Software (SPIN 2003) LNCS 2648 (2003).