The group has made significant contributions in the theoretical foundations, language formalisms, and core formal methods technology. The most important contributions in this domain are:
Logics for reasoning about quantitative artifacts
- Min-max Computation Tree Logic. P.Dasgupta, Jatindra K. Deka, P.P.Chakrabarti and S. Sriram. Artificial Intelligence, 127 (2001), 137-162.
- Quantified Computation Tree Logic. A.C.Patthak, I.Bhattacharya, A.Dasgupta, P.Dasgupta, P.P.Chakrabarti. Information Processing Letters, 82(3): 123-129, 2002.
- A Fuzzy Real Time Temporal Logic. Subhankar Mukherjee, P. Dasgupta. International Journal of Approximate Reasoning, 54(9): 1452-1470, 2013.
- Formal Assessment of Reliability Specifications in Embedded Cyber-Physical Systems. Aritra Hazra, Palab Dasgupta and Partha Pratim Chakrabarti. Accepted for Publication in the Journal of Applied Logic (JAL), Elsevier, 2016.
Auxiliary specifications - beyond temporal logic
- Auxiliary state machines + context triggered properties in verification. Ansuman Banerjee, Pallab Dasgupta, P.P. Chakrabarti. ACM Transactions on Design Automation of Electronic Systems, 13 (4), 2008, 62:1 - 62:31.
- Auxiliary Specifications for Context-Sensitive Monitoring of AMS assertions. Subhankar Mukherjee, P. Dasgupta, S. Mukhopadhyay. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 30(10): 1446-1457, 2011.
- Instrumenting AMS Assertion Verification on Commercial Platforms. Rajdeep Mukhopadhyay, S K Panda, Pallab Dasgupta, John Gough. ACM Transactions on Design Automation of Electronic Systems, 14 (2), 2009, 21:1-21:47
Methods for reasoning with formal properties
- Design Intent Coverage – A New Paradigm for Formal Property Verification. P.Basu, S.Das, A.Banerjee, P. Dasgupta, P.P. Chakrabarti, C.R. Mohan, L.Fix, R.Armoni. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 25 (10) 1922-1934,2006.
- Design Intent Coverage Revisited. Arnab Sinha, Pallab Dasgupta, Bhaskar Pal, Sayantan Das, Prasenjit Basu, P.P. Chakrabarti. ACM Transactions on Design Automation of Electronic Systems, 14 (1) 2009, 9:1—9:32.
- Time-Budgeting: A Component Based Development Methodology for Real-time Embedded Systems. Manoj Dixit, S.Ramesh and Pallab Dasgupta. Formal Aspects of Computing (FAOC), Springer, 26(3), 591-621, 2014.
Features - non Boolean functional properties
- Formal Interpretation of Assertion Based Features on AMS Designs. Antonio A Bruto Da Costa, Pallab Dasgupta. IEEE Design and Test, 32(1), 9-17 (2015).
- Feature Indented Assertions for Analog and Mixed-Signal Validation. Antara Ain, Antonio A Bruto Da Costa, Pallab Dasgupta. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, (to appear).
The group's work on logics for expressing quantitative artifacts is path-breaking and separates this work from the classical body of logic dealing with Boolean propositions and predicates. We introduced logics like Min-Max Computation Tree Logic, Quantified Computation Tree Logic, Fuzzy Real Time Temporal Logic, which have been extensively studied by other researchers. Very recently we have shown for the first time that reliability annotations on temporal logics can be used to obtain provable guarantees on reliability of component based dynamical systems.
Temporal logic based specifications are widely used in formal verification; however in practice, the task of developing formal specifications is greatly facilitated by using auxiliary formalisms. The group's work on auxiliary state machines is widely adopted in industrial practice. More recently we have shown that auxiliary automata and auxiliary functions can significantly enhance the expressive power of analog extensions of assertion languages. Our work has been used as one of the primary references in the Accellera Verilog-AMS subcommittee working towards introducing AMS assertions in Verilog-AMS standards.
Model checking techniques for formal verification primarily aim to prove formal properties on state machine representations of the design under test. Scalability is a major concern here since the state machines of real world systems are huge and (typically) do not fit in memory. In a seminal collaboration with Intel researchers, the group developed a reasoning framework, where coverage gaps between system-level properties and proven properties of components can be evaluated, thereby targeting the verification effort on specific component level properties, as opposed to the whole system. This design intent coverage methodology, was integrated into Intel's formal verification tool flow, has been jointly published, and also articulated in the monograph, "A Roadmap for Formal Property Verification", published by Springer in 2006. Later the methodology was extended to parametric reasoning for early time budgeting in component based real time automotive control systems and patented for that domain with General Motors.
In a recent work sponsored by the prestigious Semiconductor Research Corporation (SRC), the group has introduced a path-breaking concept called formal features. As opposed to assertions which have a Boolean outcome, features are real valued. Our language formalism for features enables the use of un-interpreted variables (called local variables) for computing real valued artifacts over matches of an underlying Boolean assertion. We have shown that features can express a wide range of properties in the control domain and the analog circuit domain.