Journal and Conference Articles
Static Executes-Before Analysis for Event Driven Programs.
Rekha Pai, Abhishek Uppar, Akshatha Shenoy, Pranshul Kushwaha, Deepak D'Souza.
ESEC/FSE 2022 (accepted).
Static Race Detection for Periodic Programs.
Varsha P Suresh,
Sujit Kumar Chakrabarti,
On the Expressiveness of TPTL in the Pointwise and Continous Semantics.
Raveendra Holla, Nabarun Deka, Deepak D'Souza.
GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis
over Infinite State Spaces.
Stanly Samuel, Deepak D'Souza, Raghavan Komondoor.
FSE Demo Track 2021.
- Specification Synthesis with Constrained Horn Clauses.
Sumanth Prabhu, Grigory Fedyukovich, Kumar Madhukar, Deepak
PLDI 2021 (Distinguished Paper Award).
Static analysis for detecting high-level races in RTOS kernels.
Rekha Pai, Abhishek Singh, Deepak D'Souza, Meenakshi D'Souza, Prathibha Prakash.
Formal Methods in Systems Design (FMSD), 58(1-2): 294-321, 2021.
Static Race Detection for RTOS Applications.
Rishi Tulsyan, Rekha Pai, Deepak D'Souza.
Verification of a Generative Separation Kernel.
Inzemamul Haque, Deepak D'Souza, P. Habeeb, Arnab Kundu, Ganesh Babu.
ATVA 2020, LNCS 12302, Spinger.
Verifying Band Convergence for Sampled Control Systems.
P. Ezudheen, Zahra Afzal, Pavithra Prabhakar, Deepak D'Souza, and Meenakshi D'Souza.
NASA Formal Methods (NFM) 2020.
Static Analysis for Detecting High-Level Races in RTOS Kernels.
Abhishek Singh, Rekha Pai, Deepak D'Souza, Meenakshi D'Souza.
Formal Methods Symposium (FM) 2019, LNCS 11800, Springer.
Data Races and Static Analysis for Interrupt-Driven Kernels.
Nikita Chopra, Rekha Pai, Deepak D'Souza.
ESOP 2019, LNCS 11423, Springer.
Horn-ICE learning for synthesizing invariants and contracts,
P. Ezudheen, Daniel Neider, Deepak D'Souza, Pranav Garg, P. Madhusudan.
PACMPL 2 (OOPSLA), 131:1-131:25, 2018.
- A Thread-Local Semantics and its Efficient Sequential Abstractions for Race-Free Programs,
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetsky.
24th Static Analysis Symposium (SAS) 2017.
Detecting all High-Level Dataraces in an RTOS Kernel,
Suvam Mukherjee, S. Arun Kumar, Deepak D'Souza.
Proc. 18th VMCAI, 2017.
An optimization based approach for matching applications with textual models,
Tejas Patil, Raghavan Komondoor, Deepak D'Souza and Indrajit Bhattacharya.
Proc. 32nd ICSME, 2016.
Model-checking trace-based information flow properties for infinite-state systems.
Deepak D'Souza and Raghavendra K. R.
Journal of Computer Security, vol 24(5): 617-643, 2016.
Refinement-Based Verification of the FreeRTOS Scheduler in VCC.
Sumesh Divakaran, Deepak D'Souza, Anirudh Kushwah, Prahladavaradan Sampath, Nigamanth Sridhar, and Jim Woodcock
Proc. ICFEM 2015, LNCS 9407, 170-186 (2015).
Using formal reasoning on a model of tasks for FreeRTOS,
Shu Cheng, Jim Woodcock, and Deepak D'Souza,
in Formal Aspects of Computing, volume 27, issue 1, pp 167-192, Jan 2015.
A Multi-Core Version of FreeRTOS
Verified for Datarace and Deadlock Freedom,
(with Prakash Chandrasekaran, Shibu Kumar K B, Remish L. Minz, and Lomesh Meshram),
in proc. 12th ACM-IEEE International Conference on Formal Methods and
Models for System Design (MEMOCODE) 2014.
Efficient Refinement Checking in VCC,
(with Sumesh Divakaran and Nigamanth Sridhar),
in proc. VSTTE 2014, LNCS 8471.
Using relationships for matching textual domain models with existing code.,
(with Raghavan Komondoor, Indrajit Bhattacharya, and Sachin Kale),
in proc. WCRE 2013, pp. 371-380, 2013.
A compositional hierarchical monitoring
automaton construction for LTL,
(with Raj Mohan M.),
in proc. ICTAC 2012, LNCS vol. 7521.
Temporal Logics of Repeating Values
(with Stephane Demri and Regis Gascon),
Journal of Logic and Computation,
volume 22, issue 5, pp. 1059-1096 (2012).
Model-checking bisimulation-based information flow properties for infinite state systems,
(with Raghavendra K. R.),
in proc. ESORICS, LNCS vol. 7459 (2012).
Scalable Flow-Sensitive Pointer Analysis for
Java with Strong Updates
(with Arnab De),
in proc. ECOOP 2012, LNCS 7313.
Conflict-Tolerant Specifications for
(with Madhu Gopinathan, S. Ramesh, and Prahladavaradan Sampath),
Journal of IISc, Vol. 93, No. 3, 2013.
Dataflow analysis for data-race free programs,
(with Arnab De and Rupesh Nasre),
in Proc. ESOP 2011, LNCS 6602, 2011.
Model-checking trace-based information flow properties,
Deepak D'Souza, Raveendra Holla, K. R. Raghavendra, and Barbara Sprick,
Journal of Computer Security, Vol 19, Issue 1, pp 101-138, 2011.
A Case Study in
Matching Service Descriptions to Implementations in an Existing
(with Hari S. Gupta, Raghavan Komondoor, and Girish M. Rama),
in ICSM 2010.
Analysing Message Sequence Graph Specifications
(with Joy Chakraborty and K. Narayan Kumar)
in proc. ISoLA
2010, LNCS 6415.
WOMM: A Weak Operational Memory Model,
(with Arnab De and Abhik Roychoudhury),
in proc. ISoLA 2010, LNCS 6415, pages 519-534.
- Equivalence of the Pointwise and Continuous
Semantics of First Order Logic with Linear Constraints
(with Raveendra Holla)
Specifications in Metric Temporal Logic
(with Sumesh Divakaran and Raj Mohan M.),
in proc. TIME 2010.
Conflict-Tolerant Specifications in Temporal Logic
(with Sumesh Divakaran and Raj Mohan M.), in proc. India Software
Engineering Conference (ISEC) 2010.
Deepak D'Souza, Madhu Gopinathan, S. Ramesh, and Prahladavaradan
Supervisory control for real-time systems based on
in Proc. 5th IEEE Conf. on Automation Science and
Engineering (CASE), pages 555--560, 2009.
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.
Conflict-Tolerant Real-Time Features
(with Madhu Gopinathan, S. Ramesh, and Prahladavaradan
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.
- Java Memory Model aware Software Validation
(with Arnab De and Abhik Roychoudhury)
in PASTE'08 Workshop.
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.
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.
(with Madhu Gopinathan)
in proc. 20th Int. Conference on Computer Aided
Verification (CAV) 2008, Princeton, pages 227-239.
- Counter-free input-determined timed
(with Fabrice Chevalier and Pavithra Prabhakar),
in FORMATS 2007, LNCS 4763, pp. 82--97.
A Technical Report
is also available.
- A decidable temporal logic of
(with Stephane Demri and Regis Gascon)
in Proc. Symposium on Logical Foundations of Computer
Science (LFCS) 2007, LNCS 4514, pp. 180--194.
- On continuous timed automata with
(with Fabrice Chevalier and Pavithra Prabhakar)
in Proc. FSTTCS 2006, LNCS vol. 4337, pp. 369-380, (2006).
- Checking unwinding conditions for
finite state systems
(with K. R. Raghavendra)
VERIFY 2006 Workshop (2006).
- On the expressiveness of MTL with
(with Pavithra Prabhakar)
in Proc. FORMATS 2006, LNCS 4202, pp. 322-336 (2006).
- Computing complete test graphs
for hierarchical systems
(with Madhu Gopinathan)
in Proc. IEEE SEFM 2006, pp. 70-79 (2006).
- A unification-based decision
procedure for cryptographic protocol analysis
(with Deepak Bhardwaj)
Proc. WITS 2006, pp. 221--235 (2006).
- Eventual timed automata
(with M. Raj Mohan)
FSTTCS 2005, Springer LNCS 3821, 322--344 (2005). Also available as Technical
- 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 Technical
automata-based approach to verifying information flow
(with K R Raghavendra and Barbara Sprick)
in Proc. ARSPA Workshop 2005, ENTCS
vol 135, issue 1 (2005).
- Fault diagnosis using timed
(with Patricia Bouyer and Fabrice Chevalier)
in Proc. FOSSACS 2005, LNCS 3441, pp. 219--233.
- On timed automata with input-determined
(with Nicolas Tabareau),
in Proc. FORMATS-FTRTFT 2004, LNCS 3253 (2004).
- Timed control with partial
Proc. 15th Conf. on Computer Aided Verification (CAV 2003),
LNCS 2725 (2003).
- Checking consistency of SDL+MSC
in Proc. 10th International SPIN Workshop on
Model Checking of Software (SPIN 2003) LNCS 2648 (2003).
- A Logical Characterisation of Event Clock
in Intl. Journal of Foundations of Computer Science,
Vol. 14, No. 4, World Scientific (2003),
- An Automata-Theoretic Approach to Constraint
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
Timed control synthesis for external specifications
(with P. Madhusudan)
Proc. STACS 2002, LNCS 2285, 2002.
- Product Interval Automata,
Sadhana, Academy Proceedings in Engineering Sciences,
Vol. 27, No. 2, Indian Academy of Sciences (2002), 181--208.
A Logical Characterisation of Event Recording Automata
Proc. FTRTFT 2000, LNCS 1926, 2000.
- Product Interval Automata: A
Subclass of Timed Automata
(with P. S. Thiagarajan)
Proceedings of 19th FSTTCS, LNCS 1732, 1999.
On-the-fly Verification for Product-LTL
Proceedings of Seventh National Seminar on
Theoretical Computer Science, 1997.