@article{jetley_iyer_jones_2006, title={A formal methods approach to medical device review}, volume={39}, ISSN={["1558-0814"]}, DOI={10.1109/MC.2006.113}, abstractNote={With software playing an increasingly important role in medical devices, regulatory agencies such as the US Food and Drug Administration need effective means for assuring that this software is safe and reliable. The FDA has been striving for a more rigorous engineering-based review strategy to provide this assurance. The use of mathematics-based techniques in the development of software might help accomplish this. However, the lack of standard architectures for medical device software and integrated engineering-tool support for software analysis make a science-based software review process more difficult. The research presented here applies formal modeling methods and static analysis techniques to improve the review process. Regulation of medical device software encompasses reviews of device designs (premarket review) and device performance (postmarket surveillance). The FDA's Center for Devices and Radiological Health performs the premarket review on a device to evaluate its safety and effectiveness. As part of this process, the agency reviews software development life-cycle artifacts for appropriate quality-assurance attributes, which tend to reveal little about the device software integrity.}, number={4}, journal={COMPUTER}, author={Jetley, R and Iyer, SP and Jones, PL}, year={2006}, month={Apr}, pages={61-+} }
 @inbook{lei_iyer_2005, title={An  approach to unfolding asynchronous communication protocols}, volume={3582}, ISBN={3540278826}, booktitle={FM 2005: Formal methods: International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005: proceedings (Lecture notes in computer science ; 3582)}, publisher={Berlin; New York: Springer}, author={Lei, Y. and Iyer, S. P.}, editor={J. Fitzgerald, I. J. Hayes and Tarlecki, A.Editors}, year={2005}, pages={334–349} }
 @article{cleaveland_iyer_narasimha_2005, title={Probabilistic temporal logics via the modal mu-calculus}, volume={342}, ISSN={["1879-2294"]}, DOI={10.1016/j.tcs.2005.03.048}, abstractNote={This paper presents a mu-calculus-based modal logic for describing properties of reactive probabilistic labeled transition systems (RPLTSs) and develops a model-checking algorithm for determining whether or not states in finite-state RPLTSs satisfy formulas in the logic. The logic is based on the distinction between (probabilistic) “systems” and (nonprobabilistic) “observations”: using the modal mu-calculus, one may specify sets of observations, and the semantics of our logic then enable statements to be made about the measures of such sets at various system states. The logic may be used to encode a variety of probabilistic modal and temporal logics; in addition, the model-checking problem for it may be reduced to the calculation of solutions to systems of non-linear equations. Finally, the logic induces an equivalence on RPLTSs that coincides with accepted notions of probabilistic bisimulation in the literature.}, number={2-3}, journal={THEORETICAL COMPUTER SCIENCE}, author={Cleaveland, R and Iyer, SP and Narasimha, M}, year={2005}, month={Sep}, pages={316–350} }
 @article{abdulla_baier_iyer_jonsson_2005, title={Simulating perfect channels with probabilistic lossy channels}, volume={197}, ISSN={["1090-2651"]}, DOI={10.1016/j.ic.2004.12.001}, abstractNote={We consider the problem of deciding whether an infinite-state system (expressed as a Markov chain) satisfies a correctness property with probability 1. This problem is, of course, undecidable for general infinite-state systems. We focus our attention on the model of probabilistic lossy channel systems consisting of finite-state processes that communicate over unbounded lossy FIFO channels. Abdulla and Jonsson have shown that safety properties are decidable while progress properties are undecidable for non-probabilistic lossy channel systems. Under assumptions of “sufficiently high” probability of loss, Baier and Engelen have shown how to check whether a property holds of probabilistic lossy channel system with probability 1. In this paper, we consider a model of probabilistic lossy channel systems, where messages can be lost only during send transitions. In contrast to the model of Baier and Engelen, once a message is successfully sent to channel, it can only be removed through a transition which receives the message. We show that checking whether safety properties hold with probability 1 is undecidable for this model. Our proof depends upon simulating a perfect channel, with a high degree of confidence, using lossy channels.}, number={1-2}, journal={INFORMATION AND COMPUTATION}, author={Abdulla, P and Baier, C and Iyer, SP and Jonsson, B}, year={2005}, pages={22–40} }
 @article{abdulla_iyer_nylen_2004, title={SAT-solving the coverability problem for Petri nets}, volume={24}, ISSN={["1572-8102"]}, DOI={10.1023/B:FORM.0000004786.30007.f8}, number={1}, journal={FORMAL METHODS IN SYSTEM DESIGN}, author={Abdulla, PA and Iyer, SP and Nylen, A}, year={2004}, month={Jan}, pages={25–43} }
 @article{finkel_iyer_sutre_2003, title={Well-abstracted transition systems: application to FIFO automata}, volume={181}, ISSN={["1090-2651"]}, DOI={10.1016/S0890-5401(02)00027-5}, abstractNote={Formal methods based on symbolic representations have been found to be very effective. In the case of infinite state systems, there has been a great deal of interest in accelerations —a technique for characterizing the result of iterating an execution sequence an arbitrary number of times, in a sound, but not necessarily complete, way. We propose the use of abstractions as a general framework to design accelerations. We investigate SemiLinear Regular Expressions (SLREs) as symbolic representations for FIFO automata. In particular, we show that: (a) SLREs are easy to manipulate , (b) SLREs form the core of known FIFO symbolic representations, and (c) SLREs are sufficient to represent the effect of arbitrary iterations of a loop for FIFO automata with one channel.}, number={1}, journal={INFORMATION AND COMPUTATION}, author={Finkel, A and Iyer, SP and Sutre, G}, year={2003}, month={Feb}, pages={1–31} }
 @inbook{narasimha_cleaveland_iyer_1999, title={Probabilistic temporal logics via the modal mu-calculus}, volume={1578}, ISBN={3540657193}, booktitle={Foundations of software science and computation structures: Second International Conference, FOSSACS '99 held as part of the joint European Conferences on Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999: proceedings}, publisher={Berlin; New York: Springer}, author={Narasimha, M. and Cleaveland, R. and Iyer, P.}, year={1999}, pages={288–305} }