Tutorials / Invited Talks

• Symbolic Techniques for Software Debugging Abhik Roychoudhury and Satish Chandra

  Technical Briefing at ACM/IEEE International Conference on Software Engineering (ICSE) 2012.

• Debugging as a Science, that too, for Evolving Programs, Keynote given at 3rd International Workshop on Harnessing Theories for Tool Support in Software (TTSS) 2009, a workshop held along with the International Colloqium on Theoretical Aspects of Computing (ICTAC) 2009.

• Performance Debugging of Complex Embedded Systems, Tutorial given in IEEE International Conference on VLSI Design, January 2007, Bangalore (India). Jointly with Samarjit Chakraborty.

• Synthesis and Traceability of Scenario-based Executable Models, 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) 2006, Track on Highly Reliable Software, Paphos (Cyprus).

• Interacting Process Classes, Talk given during a recent visit to  UNU-IIST in May 2006.  Different versions of this talk has been given at ICSE 2006 (May 06), IIT Kharagpur (Jan 06), the Workshop on Formal Methods for Design and Analysis of Software organized by Microsoft Research India (Oct. 05), the second Workshop on Predictable Software Component Assembly at University of Manchester (Sept. 05) and various other places.

• Software Timing Analysis, Tutorial presentation at International Conference on Formal Engineering Methods (ICFEM) November 2005, Manchester (UK).

• Scenario based methods for System design Invited Tutorial presentation at International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN '05), Miami (USA), June 2005. Jointly with P.S. Thiagarajan.

• Program Transformations for Automated Verification


(ppt slides, pdf [4 slides/page for printing])
Invited tutorial at the International Conference on Logic Programming (ICLP) 2002, Copenhagen (Denmark).  Jointly with I.V. Ramakrishnan.
Relevant papers: PPDP99, TACAS00, CAV01.
Download the prover: Code (Gzipped tar), Examples (Gzipped tar), README (plain text).

Conference Presentations and Recent Visits

• DARWIN: an approach for debugging evolving programs,
  Visit to Fraunhofer Center for Software Engineering and University of Maryland (Dec 2009), SRI (July 2010), ...
  A similar talk was given at ESEC-FSE 2009 for the conference presentation of the paper which received the Distinguished Paper Award.
  
• Timing analysis of embedded software,
  At TU Dortmund, Germany, August 2009. Similar talks have been given at TU Munich (2010) and Universitat des Saarlandes (2010), ...
  
• Dynamic Slicing of Java Programs,
  Visit to Kings College London, July 2007.
  
• Hierarchical Dynamic Slicing (pdf slides)
  Paper presented at ISSTA 2007, London, UK.
  
• Memory Model Sensitive Bytecode Verificaton (pdf slides)
  Paper presented at FM 06, Hamilton, Canada. The slides are from an extended talk on the same topic given at Microsoft Research India in January 2007.
  
• Modeling Out-of-Order Processors for Software Timing Analysis (pdf slides)
  Paper presented at RTSS 2004, Lisbon, Portugal.
  
• Automatic Generation of Protocol Converters from Scenario-based Specifications (pdf slides)
  Paper presented at RTSS 2004, Lisbon, Portugal.
  
• Symbolic Execution of Behavioral Requirements (pdf slides)
  Paper presented at PADL 2004, Dallas, USA.
  
• Compactly Representing Parallel Program Executions, (ppt slides),

Paper presented at PPoPP 2003, San Diego (California), USA.

• Accurate Timing Analysis by Modeling Caches, Speculation and their Interaction, (ppt slides),

Paper presented at DAC 2003, Anaheim (California), USA.

• Using formal techniques to debug the AMBA System-on-Chip Bus Protocol (ppt slides),

Paper presented at IEEE Conference on Design, Automation and Test in Europe (DATE) 2003, Munich, Germany.
SMV Source Code

• Reasoning about Hardware and Software Memory Models (ppt slides),

Paper presented at International Conference on Formal Engineering Methods (ICFEM) 2002, Shanghai, China.

• Specifying Multithreaded Java semantics for program verification (ppt),

Paper presented at the International Conference on Software Engineering (ICSE) 2002, Orlando, USA.
Download the checker:  Code & Examples (Gzipped tar file),  README (plain text)

• Auotomated Inductive Verification of Parameterized Protocols (ps)

Paper presented at the International Conference on Computer Aided Verification (CAV) 2001, Paris, France.

• Program Transformations for Verifying Parameterized Systems (ps)

Slides from my doctoral dissertation talk, December 2000, State University of New York at Stony Brook, New York, USA.

• Unfold/fold Transformations of Logic Programs (ps)

A talk given at the New England Seminar on Programming Languages and Systems, December 2000, Brown University, Rhode Island, USA.

• Justifying Proofs using Memo Tables (ps)

Paper presented at the International Conference on Principles and Practice of Declarative Programming (PPDP) 2000, Montreal, Canada.

• A Parameterized Unfold/Fold Transformation Framework for Definite Logic Programs (ps)

Paper presented at the International Conference on Principles and Practice of Declarative Programming (PPDP) 1999, Paris, France.

Last updated 21 June 2008.