Centre for Formal Design & Verification of Software
CFDVS: A Quick Introduction
Computers in Safety-Critical Systems
Nuclear reactors, chemical plants, avionics, medical care, space missions, railway signaling, ...
Enormous cost of failures induced by bugs
Loss of lives, environmental and infrastructure damage, Financial loss, scientific setbacks, ...
Corner-case bugs in software and hardware Extremely hard to detect
May escape extended testing – infeasible to test all cases Can cause catastrophic failure of safety-critical systems
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Computers in Safety-Critical Systems
Nuclear reactors, chemical plants, avionics, medical care, space missions, railway signaling, ...
Enormous cost of failures induced by bugs
Loss of lives, environmental and infrastructure damage, Financial loss, scientific setbacks, ...
Corner-case bugs in software and hardware Extremely hard to detect
May escape extended testing – infeasible to test all cases Can cause catastrophic failure of safety-critical systems
Computers in Safety-Critical Systems
Nuclear reactors, chemical plants, avionics, medical care, space missions, railway signaling, ...
Enormous cost of failures induced by bugs
Loss of lives, environmental and infrastructure damage, Financial loss, scientific setbacks, ...
Corner-case bugs in software and hardware Extremely hard to detect
May escape extended testing – infeasible to test all cases Can cause catastrophic failure of safety-critical systems
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Some Infamous Computer Bugs
Therac-25 administers lethal radiation to patients (1985-87) Bug in software controller
Pentium FDIV bug costs Intel US$475 million (1994) Bug in lookup-table of algorithm
Ariane 5 rocket explodes a minute after launch (1996) Software overflow bug
NASA’s Mars Climate Orbiter veers off and disintegrates (1999) Software bug controlling spacecraft’s motion
Toyota Prius hybrid cars grind to halt unexpectedly (2015) Software bug in car’s embedded controllers
Airbus A400M military transport aircraft crashes (2015) Bug in software configuration
Nest’s IoT-enabled thermostat freezes homes in peak winter (2016)
Role of Formal Methods
Complexity of systems makes it humanly impossible to identify All corner case inputs for software & hardware
Long sequences of inputs that can lead to failure
Testing still pre-dominant method of validation in industry
Strength: Easier to generate test inputs, actual system can be tested Weakness: Confidence only as good as test suite
E. W. Dijkstra: “Program testing can be used to show the presence of bugs, but never their absence.”
Complementary role of formal verification
Strength: Comprehensive, no test inputs, catches all bugs that exist Weakness: Computationally harder, requires greater expertise, only models verified
Mandatory step before chip tape-out in Intel, AMD, Fujitsu, ... Software companies rapidly adopting formal methods (Microsoft, IBM, TCS, ...)
Significant progress in last 30 years
Multiple Turing Awards for work related to formal verification Formal verification tool-chains internally developed in several companies
Formal verification tools available commercially & in public-domain
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Role of Formal Methods
Complexity of systems makes it humanly impossible to identify All corner case inputs for software & hardware
Long sequences of inputs that can lead to failure
Testing still pre-dominant method of validation in industry
Strength: Easier to generate test inputs, actual system can be tested Weakness: Confidence only as good as test suite
E. W. Dijkstra: “Program testing can be used to show the presence of bugs, but never their absence.”
Complementary role of formal verification
Strength: Comprehensive, no test inputs, catches all bugs that exist Weakness: Computationally harder, requires greater expertise, only models verified
Mandatory step before chip tape-out in Intel, AMD, Fujitsu, ... Software companies rapidly adopting formal methods (Microsoft, IBM, TCS, ...)
Significant progress in last 30 years
Multiple Turing Awards for work related to formal verification Formal verification tool-chains internally developed in several companies
Formal verification tools available commercially & in public-domain
Role of Formal Methods
Complexity of systems makes it humanly impossible to identify All corner case inputs for software & hardware
Long sequences of inputs that can lead to failure
Testing still pre-dominant method of validation in industry
Strength: Easier to generate test inputs, actual system can be tested Weakness: Confidence only as good as test suite
E. W. Dijkstra: “Program testing can be used to show the presence of bugs, but never their absence.”
Complementary role of formal verification
Strength: Comprehensive, no test inputs, catches all bugs that exist Weakness: Computationally harder, requires greater expertise, only models verified
Mandatory step before chip tape-out in Intel, AMD, Fujitsu, ... Software companies rapidly adopting formal methods (Microsoft, IBM, TCS, ...)
Significant progress in last 30 years
Multiple Turing Awards for work related to formal verification Formal verification tool-chains internally developed in several companies
Formal verification tools available commercially & in public-domain
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Role of Formal Methods
Complexity of systems makes it humanly impossible to identify All corner case inputs for software & hardware
Long sequences of inputs that can lead to failure
Testing still pre-dominant method of validation in industry
Strength: Easier to generate test inputs, actual system can be tested Weakness: Confidence only as good as test suite
E. W. Dijkstra: “Program testing can be used to show the presence of bugs, but never their absence.”
Complementary role of formal verification
Strength: Comprehensive, no test inputs, catches all bugs that exist Weakness: Computationally harder, requires greater expertise, only models verified
Mandatory step before chip tape-out in Intel, AMD, Fujitsu, ...
Software companies rapidly adopting formal methods (Microsoft, IBM, TCS, ...)
Significant progress in last 30 years
Multiple Turing Awards for work related to formal verification Formal verification tool-chains internally developed in several companies
Formal verification tools available commercially & in public-domain
Role of Formal Methods
Complexity of systems makes it humanly impossible to identify All corner case inputs for software & hardware
Long sequences of inputs that can lead to failure
Testing still pre-dominant method of validation in industry
Strength: Easier to generate test inputs, actual system can be tested Weakness: Confidence only as good as test suite
E. W. Dijkstra: “Program testing can be used to show the presence of bugs, but never their absence.”
Complementary role of formal verification
Strength: Comprehensive, no test inputs, catches all bugs that exist Weakness: Computationally harder, requires greater expertise, only models verified
Mandatory step before chip tape-out in Intel, AMD, Fujitsu, ...
Software companies rapidly adopting formal methods (Microsoft, IBM, TCS, ...)
Significant progress in last 30 years
Multiple Turing Awards for work related to formal verification Formal verification tool-chains internally developed in several companies
Formal verification tools available commercially & in public-domain
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Formal Verification in a Nutshell
System Modeling: Given a system, derive amathematically precise description of what it does
Automata, process calculi, programs, logics, circuits, ...
Automatically derived and/or manually constructed
Property Specification: Amathematically precisedescription of what the system is supposed to do
Unambiguous objective interpretation
Automata, logics, constraint languages, structured English, ... Free English can be ambiguous and not suitable
Verification Techniques: Computational techniquesto check if modelsatisfiesspecification
Curse of undecidability
General algorithms:mathematical impossibility
(Semi-)algorithms for practically relevant sub-classes of problems Tools require significant engineering
Theorem proving
Axioms and inference rule schemas for specific logics
Apply (semi-)automatically to derive consequence from premises Model checking
Algorithmically check if all runs of model satisfy specification Admits automation for special classes of problems.
Hybrid techniques: intelligent combinations of above
Formal Verification in a Nutshell
System Modeling: Given a system, derive amathematically precise description of what it does
Automata, process calculi, programs, logics, circuits, ...
Automatically derived and/or manually constructed
Property Specification: Amathematically precisedescription of what the system is supposed to do
Unambiguous objective interpretation
Automata, logics, constraint languages, structured English, ...
Free English can be ambiguous and not suitable
Verification Techniques: Computational techniquesto check if modelsatisfiesspecification
Curse of undecidability
General algorithms:mathematical impossibility
(Semi-)algorithms for practically relevant sub-classes of problems Tools require significant engineering
Theorem proving
Axioms and inference rule schemas for specific logics
Apply (semi-)automatically to derive consequence from premises Model checking
Algorithmically check if all runs of model satisfy specification Admits automation for special classes of problems.
Hybrid techniques: intelligent combinations of above
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Formal Verification in a Nutshell
System Modeling: Given a system, derive amathematically precise description of what it does
Automata, process calculi, programs, logics, circuits, ...
Automatically derived and/or manually constructed
Property Specification: Amathematically precisedescription of what the system is supposed to do
Unambiguous objective interpretation
Automata, logics, constraint languages, structured English, ...
Free English can be ambiguous and not suitable
Verification Techniques: Computational techniquesto check if modelsatisfiesspecification
Curse of undecidability
General algorithms:mathematical impossibility
(Semi-)algorithms for practically relevant sub-classes of problems Tools require significant engineering
Theorem proving
Axioms and inference rule schemas for specific logics
Apply (semi-)automatically to derive consequence from premises Model checking
Algorithmically check if all runs of model satisfy specification Admits automation for special classes of problems.
Hybrid techniques: intelligent combinations of above
Formal Verification in a Nutshell
System Modeling: Given a system, derive amathematically precise description of what it does
Automata, process calculi, programs, logics, circuits, ...
Automatically derived and/or manually constructed
Property Specification: Amathematically precisedescription of what the system is supposed to do
Unambiguous objective interpretation
Automata, logics, constraint languages, structured English, ...
Free English can be ambiguous and not suitable
Verification Techniques: Computational techniquesto check if modelsatisfiesspecification
Curse of undecidability
General algorithms:mathematical impossibility
(Semi-)algorithms for practically relevant sub-classes of problems Tools require significant engineering
Theorem proving
Axioms and inference rule schemas for specific logics
Apply (semi-)automatically to derive consequence from premises Model checking
Algorithmically check if all runs of model satisfy specification Admits automation for special classes of problems.
Hybrid techniques: intelligent combinations of above
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Formal Verification in a Nutshell
System Modeling: Given a system, derive amathematically precise description of what it does
Automata, process calculi, programs, logics, circuits, ...
Automatically derived and/or manually constructed
Property Specification: Amathematically precisedescription of what the system is supposed to do
Unambiguous objective interpretation
Automata, logics, constraint languages, structured English, ...
Free English can be ambiguous and not suitable
Verification Techniques: Computational techniquesto check if modelsatisfiesspecification
Curse of undecidability
General algorithms:mathematical impossibility
(Semi-)algorithms for practically relevant sub-classes of problems Tools require significant engineering
Theorem proving
Axioms and inference rule schemas for specific logics
Apply (semi-)automatically to derive consequence from premises
Model checking
Algorithmically check if all runs of model satisfy specification Admits automation for special classes of problems.
Hybrid techniques: intelligent combinations of above
Formal Verification in a Nutshell
System Modeling: Given a system, derive amathematically precise description of what it does
Automata, process calculi, programs, logics, circuits, ...
Automatically derived and/or manually constructed
Property Specification: Amathematically precisedescription of what the system is supposed to do
Unambiguous objective interpretation
Automata, logics, constraint languages, structured English, ...
Free English can be ambiguous and not suitable
Verification Techniques: Computational techniquesto check if modelsatisfiesspecification
Curse of undecidability
General algorithms:mathematical impossibility
(Semi-)algorithms for practically relevant sub-classes of problems Tools require significant engineering
Theorem proving
Axioms and inference rule schemas for specific logics
Apply (semi-)automatically to derive consequence from premises Model checking
Algorithmically check if all runs of model satisfy specification Admits automation for special classes of problems.
Hybrid techniques: intelligent combinations of above
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Formal Verification in a Nutshell
System Modeling: Given a system, derive amathematically precise description of what it does
Automata, process calculi, programs, logics, circuits, ...
Automatically derived and/or manually constructed
Property Specification: Amathematically precisedescription of what the system is supposed to do
Unambiguous objective interpretation
Automata, logics, constraint languages, structured English, ...
Free English can be ambiguous and not suitable
Verification Techniques: Computational techniquesto check if modelsatisfiesspecification
Curse of undecidability
General algorithms:mathematical impossibility
(Semi-)algorithms for practically relevant sub-classes of problems Tools require significant engineering
Theorem proving
Axioms and inference rule schemas for specific logics
Apply (semi-)automatically to derive consequence from premises
Everyday Reality of Formal Verification
[Courtesy:Computers and Intractibility: A Guide to the Theory of NP-Completeness, M.R. Garey and D.S. Johnson, 1979]
Nevertheless, safety-critical systems must verifiably satisfy their specs Carving out relevant sub-problems crucial
Domain knowledge invaluable Engineering optimizations essential
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Everyday Reality of Formal Verification
[Courtesy:Computers and Intractibility: A Guide to the Theory of NP-Completeness, M.R. Garey and D.S. Johnson, 1979]
Nevertheless, safety-critical systems must verifiably satisfy their specs
Carving out relevant sub-problems crucial Domain knowledge invaluable
Engineering optimizations essential
Everyday Reality of Formal Verification
[Courtesy:Computers and Intractibility: A Guide to the Theory of NP-Completeness, M.R. Garey and D.S. Johnson, 1979]
Nevertheless, safety-critical systems must verifiably satisfy their specs Carving out relevant sub-problems crucial
Domain knowledge invaluable Engineering optimizations essential
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Brief History of CFDVS
1999: DAE sets up CFDVS, recognizing crucial role of formal methods in safety-critical systems
MoU between IIT Bombay, TIFR and BARC Rs. 3 crore financial support from BRNS 1999-2009: CFDVS Phase 1
Development of formal property verification technologies Independent V&V projects from
Government agencies: DRDL, ADA, VSSCC, BARC, ...
Private agencies: Microsoft Research, General Motors, Texas Instruments, Intel, ...
Manpower training: Workshops, CEP courses, student projects Course material development in formal verification
Brief History of CFDVS
2010-2017: CFDVS Phase 2
Rs. 3 crore financial support from BRNS
3 concrete sub-projects on formal specificationandverificationof computer systems
1 Reachability of “unsafe” states in sequential circuits
2 Assertion checking for programs in a subset of C
3 Requirements modeling and analysis: unifying diverse formalisms
Focus on developing theory and tools that push boundaries of state-of-the-art
Improve precision of analysis, without significantly degrading performance
Exploit parallel computation
Enable analysis not available in today’s tools Concrete tool deliverables for each sub-project
Significanttheoretical and tool developmentcomponents
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Brief History of CFDVS
2010-2017: CFDVS Phase 2
Rs. 3 crore financial support from BRNS
3 concrete sub-projects on formal specificationandverificationof computer systems
1 Reachability of “unsafe” states in sequential circuits
2 Assertion checking for programs in a subset of C
3 Requirements modeling and analysis: unifying diverse formalisms Focus on developing theory and tools that push boundaries of state-of-the-art
Improve precision of analysis, without significantly degrading performance
Exploit parallel computation
Enable analysis not available in today’s tools Concrete tool deliverables for each sub-project
Brief History of CFDVS
2017-present: CFDVS Phase 3 IMPRINT projects
1 FMSAFE: IIT Kharagpur, IIT Bombay and IIT Kanpur Formal methods for different sectors in Indian govt & industry
2 Remote healthcare delivery system: IIT Kharagpur, IIT Bombay, AIIMS, IoTimize and Azure Systems
Diagnostic aid with machine learning and formal methods
Ashutosh’ project with German collaborators Krishna and Akshay’s CEFIPRA projects
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
CFDVS (Multi-institutional collaborations)
IMPRINT projects
Collaborators: IIT Kharagpur, AIIMS, IIT Kanpur
Systems biology
Finding gene regulatory pathways that explain wet-lab experiments Collaborators: ACTREC, Tata Memorial Centre
Logic and automata theory
Akshay and Krishna’s CEFIPRA projects Collaborators: LSV, ENS Cachan Constrained sampling and counting
How do we count solutions of constraints? How do we sample uniformly from solution space?
Without generating all solutions With strong approximation guarantees
Collaborators: Rice University, National Univ. of Singapore Concurrent software verification
Ashutosh’ ongoing collaboration Collaborators: MPI-SWS
CFDVS (Multi-institutional collaborations)
IMPRINT projects
Collaborators: IIT Kharagpur, AIIMS, IIT Kanpur Systems biology
Finding gene regulatory pathways that explain wet-lab experiments Collaborators: ACTREC, Tata Memorial Centre
Logic and automata theory
Akshay and Krishna’s CEFIPRA projects Collaborators: LSV, ENS Cachan Constrained sampling and counting
How do we count solutions of constraints? How do we sample uniformly from solution space?
Without generating all solutions With strong approximation guarantees
Collaborators: Rice University, National Univ. of Singapore Concurrent software verification
Ashutosh’ ongoing collaboration Collaborators: MPI-SWS
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
CFDVS (Multi-institutional collaborations)
IMPRINT projects
Collaborators: IIT Kharagpur, AIIMS, IIT Kanpur Systems biology
Finding gene regulatory pathways that explain wet-lab experiments Collaborators: ACTREC, Tata Memorial Centre
Logic and automata theory
Akshay and Krishna’s CEFIPRA projects Collaborators: LSV, ENS Cachan
Constrained sampling and counting
How do we count solutions of constraints? How do we sample uniformly from solution space?
Without generating all solutions With strong approximation guarantees
Collaborators: Rice University, National Univ. of Singapore Concurrent software verification
Ashutosh’ ongoing collaboration Collaborators: MPI-SWS
CFDVS (Multi-institutional collaborations)
IMPRINT projects
Collaborators: IIT Kharagpur, AIIMS, IIT Kanpur Systems biology
Finding gene regulatory pathways that explain wet-lab experiments Collaborators: ACTREC, Tata Memorial Centre
Logic and automata theory
Akshay and Krishna’s CEFIPRA projects Collaborators: LSV, ENS Cachan Constrained sampling and counting
How do we count solutions of constraints? How do we sample uniformly from solution space?
Without generating all solutions With strong approximation guarantees
Collaborators: Rice University, National Univ. of Singapore
Concurrent software verification Ashutosh’ ongoing collaboration Collaborators: MPI-SWS
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
CFDVS (Multi-institutional collaborations)
IMPRINT projects
Collaborators: IIT Kharagpur, AIIMS, IIT Kanpur Systems biology
Finding gene regulatory pathways that explain wet-lab experiments Collaborators: ACTREC, Tata Memorial Centre
Logic and automata theory
Akshay and Krishna’s CEFIPRA projects Collaborators: LSV, ENS Cachan Constrained sampling and counting
How do we count solutions of constraints? How do we sample uniformly from solution space?
Without generating all solutions With strong approximation guarantees
Collaborators: Rice University, National Univ. of Singapore Concurrent software verification
CFDVS: Some Recent Tools Developed
ParMC
Parallel portfolio model checker for checking reachability of “unsafe”
states in sequential circuits CAnalyzer
User-configurable multi-abstract-domain multi-threaded assertion checker for a subset of C
TARA
Concurrent software verification with relaxed memory models DCTools
Unifying diverse specification formalisms with rich analysis support Word-level hardware verification
VBMC: Word-level VHDL Bounded Model Checker STEWord: Word-level Symbolic Trajectory Eval (with Intel) Optimizing solving word constraints with multiplication
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
CFDVS Phase 2: Tools Developed
Scalable constrained sampling & counting (with Rice University) Varied applications (test generation, quantified information flow, ...) UniGen2: Scalable constrained sampler with guarantees
ApproxMC2: Scalable constrained model counter with guarantees SPLanE (with INRIA and GM Research)
Framework for formally specifying, analyzing and verifying software product lines
CParCegar
Boolean functional synthesis from relational specifications Varied applications (inverting one-way functions, state machine decomposition, plant controller synthesis ...)
BioNetAnalyzer (with ACTREC, TMC)
Discovery and formal analysis of bio-regulatory pathways from
Importance of Theoretical Investigations
Formal verification gives rigorous theoretical guarantees
Theory is the cornerstone of our tools
Algorithms must provably work in all cases of sub-class of problems Intricate dependency of models, specification formalisms and algorithms
Correctness and performance guarantees crucial Without sound theory, formal methods are of no use End-user often oblivious of theoretical underpinnings
Effort required for solving theoretical problems under-appreciated Yet, theoretical challenges take no less time to overcome as tool building
Practical formal methods
One foot in theory, one foot in systems
Significant effort at CFDVS goes in theoretical investigations Not focus of this presentation
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Importance of Theoretical Investigations
Formal verification gives rigorous theoretical guarantees Theory is the cornerstone of our tools
Algorithms must provably work in all cases of sub-class of problems Intricate dependency of models, specification formalisms and algorithms
Correctness and performance guarantees crucial Without sound theory, formal methods are of no use
End-user often oblivious of theoretical underpinnings
Effort required for solving theoretical problems under-appreciated Yet, theoretical challenges take no less time to overcome as tool building
Practical formal methods
One foot in theory, one foot in systems
Significant effort at CFDVS goes in theoretical investigations Not focus of this presentation
Importance of Theoretical Investigations
Formal verification gives rigorous theoretical guarantees Theory is the cornerstone of our tools
Algorithms must provably work in all cases of sub-class of problems Intricate dependency of models, specification formalisms and algorithms
Correctness and performance guarantees crucial Without sound theory, formal methods are of no use End-user often oblivious of theoretical underpinnings
Effort required for solving theoretical problems under-appreciated Yet, theoretical challenges take no less time to overcome as tool building
Practical formal methods
One foot in theory, one foot in systems
Significant effort at CFDVS goes in theoretical investigations Not focus of this presentation
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Importance of Theoretical Investigations
Formal verification gives rigorous theoretical guarantees Theory is the cornerstone of our tools
Algorithms must provably work in all cases of sub-class of problems Intricate dependency of models, specification formalisms and algorithms
Correctness and performance guarantees crucial Without sound theory, formal methods are of no use End-user often oblivious of theoretical underpinnings
Effort required for solving theoretical problems under-appreciated Yet, theoretical challenges take no less time to overcome as tool building
Practical formal methods
One foot in theory, one foot in systems
Significant effort at CFDVS goes in theoretical investigations Not focus of this presentation
Importance of Theoretical Investigations
Formal verification gives rigorous theoretical guarantees Theory is the cornerstone of our tools
Algorithms must provably work in all cases of sub-class of problems Intricate dependency of models, specification formalisms and algorithms
Correctness and performance guarantees crucial Without sound theory, formal methods are of no use End-user often oblivious of theoretical underpinnings
Effort required for solving theoretical problems under-appreciated Yet, theoretical challenges take no less time to overcome as tool building
Practical formal methods
One foot in theory, one foot in systems
Significant effort at CFDVS goes in theoretical investigations Not focus of this presentation
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Other CFDVS Activities (Beyond Tools ...)
Dissemination of research results (theory + tools) Papers, technical reports, software releases, invited talks
Phase 2: 50 technical papers, book chapter in top international fora Several invited talks at national and international venues
Teaching and man-power development
Formal methods related courses in Dept. of CSE, IIT Bombay 3 UG core courses, 4 PG elective courses
B.Tech., M.Tech. and Ph.D. student guidance (IIT Bombay, HBNI) 15 M.Tech. and 4 Ph.D. dissertations completed in Phase 2
Two winners of Excellence in Ph.D. Thesis Work in CSE, IIT Bombay 8 ongoing Ph.D. dissertations
Collaboration with industry and government organizations ADA, DRDL, VSSCC, DRDO, ...
Microsoft Research, GM Research, Intel, IBM, TRDDC, ...
Collaboration with other academic institutions
Core Competency of CFDVS
Formal specification, analysis and verification of computational systems (software, hardware, embedded, biological)
Developing theory and tools for pushing state-of-the-art in property specificaiton and model checking
Applying tools and techniques to problems from government and industry that fall in this domain
Training and manpower development in formal methods
Centre for Formal Design & Verification of Software CFDVS: A Quick Introduction
Acknowledgements
DAE and BRNS
Unstinting support and encouragement over 17 years
Bold decisions, viz. supporting post-doctoral scientists and technical assistance from visiting experts, paid rich dividends
Administration of partner institutions (IITB, TIFR, BARC) Facilitating intense collaboration and interactions
Students and staff
Cordial lab environment crucial to success Primary workhorses, who often remain un-named Collaborators from industry and government organizations
Primary source of real-life problems Sustained interaction over extended periods Deeper engagement beyond providing funds
