@article{ALLMU:DAES08,
author = {Myla Archer and Hongping Lim and Nancy Lynch and Sayan Mitra and Shinya Umeno},
title = {Specifying and proving properties of timed I/O automata using Tempo},
booktitle = {ACM Transactions on Embedded Computing Systems},
year = 2008,
publisher = {Springer Netherlands},
doi ={10.1007/s10617-008-9022-2},
month ={June},
volume ={12},
number = {1-2},
url = {http://springerlink.com/content/a82q782044162874/}
}
@article{MLL:TECS08,
author = {Sayan Mitra and Daniel Liberzon and Nancy Lynch},
title = {Verifying Average Dwell Time of Hybrid Systems},
booktitle = {ACM Transactions on Embedded Computing Systems},
year = 2008,
publisher = {ACM},
url = {}
}
@inproceedings{MC:FORMATS08,
author = {K. Mani Chandy and Sayan Mitra and Concetta Pilotto},
title = {Convergence Verification: From Shared Memory to Partially Synchronous Systems},
booktitle = {In proceedings of Formal Modeling and Analysis of Timed Systems ({FORMATS}`08)},
year = 2008,
series = {LNCS},
volume = {5215},
pages = {217--231},
publisher = {Springer Verlag},
url = {http://ist.caltech.edu/~mitras/research/2008/paper8-final.pdf}
}
@inproceedings{MC:TPHOLS08,
author = {Sayan Mitra and K. Mani Chandy},
title = {A Formalized Theory for Verifying Stability and Convergence of Automata in {PVS}},
booktitle = {In proceedings of {T}heorem {P}roving in {H}igher {O}rder {L}ogics ({TPHOLS}`08)},
year = 2008,
series = {LNCS},
volume = {5170},
pages = {230--245},
publisher = {Springer},
url = {http://ist.caltech.edu/~mitras/research/paper45.pdf}
}
@article{ML:ENTCS07,
author = {Sayan Mitra and Nancy Lynch},
title = {Proving approximate implementation relations for Probabilistic {I/O} Automata.},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
volume = 174,
NUMBER = 8,
year = 2007,
PAGES = {71-93},
EE = {}
}
@inproceedings{ML:paul06,
author = {Sayan Mitra and Nancy Lynch},
title = { Approximate simulations for task-structured probabilistic {I/O} automata},
booktitle = { LICS workshop on Probabilistic Automata and Logics (PAul06)},
year = 2006,
address = {Seattle, WA},
month = {August},
url = {http://theory.lcs.mit.edu/~mitras/research/PAul06-final.pdf}
}
@inproceedings{ALLMU:memocode06,
author = {Myla Archer and HongPing Lim and Nancy Lynch and Sayan Mitra and Shinya Umeno},
title = { Specifying and Proving Properties of Timed {I/O} Automata in the {TIOA} Toolkit },
booktitle = {In Fourth ACM-IEEE International Conference on Formal Methods
and Models for Codesign (MEMOCODE'06)},
year = 2006,
publisher = {IEEE},
url = {http://theory.lcs.mit.edu/~mitras/research/memocode06.pdf}
}
@article{MitraA05,
author = {Sayan Mitra and Myla Archer},
title = {{PVS} Strategies for Proving Abstraction Properties of Automata.},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
volume = 125,
NUMBER = 2,
year = 2005,
PAGES = {45-65},
EE = {http://dx.doi.org/10.1016/j.entcs.2005.01.005},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{ML:CDC04,
author = {Sayan Mitra and Daniel Liberzon},
title = {Stability of hybrid automata with average dwell time: an invariant approach},
booktitle = {Proceedings of the 43rd {IEEE} Conference on Decision and Control},
month = {February},
year = {2005},
address = {Paradise Island, Bahamas},
note = {Full version \url{http://theory.lcs.mit.edu/~mitras/research/cdc04-full.ps.gz}{[ps]}},
url = {http://theory.lcs.mit.edu/~mitras/research/cdc04.ps.gz}
}
@inproceedings{MA04strat,
author = {Sayan Mitra and Myla Archer},
title = {Reusable PVS Proof Strategies for Proving Abstraction Properties of {I}/{O} Automata},
booktitle = {STRATEGIES 2004, IJCAR Workshop on strategies in automated deduction},
year = {2004},
address = {Cork, Ireland},
month = {July},
url = {http://theory.lcs.mit.edu/~mitras/research/strategieso4.ps.gz}
}
@mastersthesis{mitra01masters,
author = {Sayan Mitra},
title = {{HIOA} - A Specification Language for Hybrid {I}nput/{O}utput
Automata},
school = {Department of Computer Science and Automation, IISc},
address = {Indian Institute of Science, Bangalore},
year = 2001,
url = {http://theory.lcs.mit.edu/~mitras/research/mastersthesis.ps.gz}
}
@TECHREPORT{quantr02,
author = {Sayan Mitra and Yong Wang and Nancy Lynch and Eric Feron},
title = {Application of {H}ybrid {I/O} {A}utomata in Safety Verification of
Pitch Controller for Model Helicopter System},
INSTITUTION = {MIT Laboratory for Computer Science},
year = {2002},
address = {Cambridge, MA 02139},
month = {October},
url = {http://theory.lcs.mit.edu/~mitras/research/QuanTR02.ps}
}
@inproceedings{MWLF-hscc03,
author = {Sayan Mitra and Yong Wang and Nancy Lynch and Eric Feron},
title = {Safety Verification of Model Helicopter Controller using Hybrid
{I}nput/{O}utput Automata},
booktitle = {HSCC'03, Hybrid System: Computation and Control},
address = {Prague, the Czech Republic},
month = {April 3-5},
year = {2003},
url = {http://theory.lcs.mit.edu/~mitras/research/paper033.ps}
}
@inproceedings{KLM04,
author = {Dilsun Kaynar and Nancy Lynch and Sayan Mitra},
title = {Specifying and Proving Timing Properties with {TIOA} Tools},
booktitle = {In the work in progress session of the 25th {IEEE} International
Real-Time Systems Symposium ({RTSS-WIP})},
year = {2004},
address = {Lisbon, Portugal},
month = {December},
url = {http://theory.lcs.mit.edu/~mitras/research/wip04.ps.gz}
}
@inproceedings{CLMT:disc05,
author = {Gregory Chockler and Nancy Lynch and Sayan Mitra and Joshua Tauber},
title = { Proving atomicity: an assertional approach},
booktitle = {Proceedings of Nineteenth International Symposium on Distributed Computing ({DISC'05})},
PAGES = {152 - 168},
year = 2005,
editor = {Pierre Fraigniaud},
volume = { 3724},
series = {Lecture Notes in Computer Science},
address = { Cracow, Poland },
month = {September},
publisher = {Springer},
note = {Full version:\url{http://theory.lcs.mit.edu/~mitras/research/v30.pdf}},
url = {http://theory.lcs.mit.edu/~mitras/research/disc05.pdf}
}
@inproceedings{LKLM:formats05,
author = {Hongping Lim and Dilsun Kaynar and Nancy Lynch and Sayan Mitra},
title = {Translating timed I/O automata specifications for theorem proving in PVS},
booktitle = {Proceedings of Formal Modelling and Analysis of Timed Systems ({FORMATS'05})},
year = 2005,
volume = 3829,
series = {LNCS},
address = {Uppsala, Sweden},
month = {September},
publisher = {Springer},
url = {http://theory.lcs.mit.edu/~mitras/research/formats05.pdf}
}
@inproceedings{LML:icnp05,
author = {Ben Leong and Sayan Mitra and Barbara Liskov},
title = {Path vector face routing: Geographic routing with local face information},
booktitle = { Proceedings of 13th {IEEE} International Conference on Network Protocols ({ICNP'05})},
year = 2005,
address = {Boston, Massachusetts},
month = {November},
url = {http://theory.lcs.mit.edu/~mitras/research/icnp-pvfr.pdf}
}
@inproceedings{LMN:cdc05,
author = {Nancy Lynch and Sayan Mitra and Tina Nolte},
title = {Motion coordination using virtual nodes},
booktitle = { Proceedings of 44th {IEEE} Conference on Decision and Control ({CDC05})},
year = 2005,
address = {Seville, Spain},
month = {December},
url = {http://theory.lcs.mit.edu/~mitras/research/vn-cdc07.pdf}
}
@MANUAL{TIOALanguage,
title = {{TIOA} Language},
author = {D. Kaynar and N. Lynch and S. Mitra and S. Garland},
organization = {MIT Computer Science and Artificial Intelligence Laboratory},
address = {Cambridge, MA},
year = {2005},
url = {http://tioa.csail.mit.edu/moin.cgi/ProjectDocuments/}
}
@inproceedings{MLL:hscc06,
author = {Sayan Mitra and Daniel Liberzon and Nancy Lynch},
title = {Verifying Average Dwell Time by Solving Optimization Problems},
booktitle = {Hybrid Systems: Computation and Control (HSCC 06)},
key = {mllhscc06},
year = {2006},
editor = {Ashish Tiwari and Joao P. Hespanha},
series = {LNCS},
address = {Santa Barbara, CA},
month = {March},
publisher = {Springer},
url = {http://theory.lcs.mit.edu/~mitras/research/paper033.ps}
}
@phdthesis{Mitra07PhD,
author = {Sayan Mitra},
title ={A Verification Framework for Hybrid Systems},
year = {2007},
month = {September},
school = {Massachusetts Institute of Technology},
address = {Cambridge, MA 02139},
url = {http://people.csail.mit.edu/mitras/research/thesis.pdf}
}
@inproceedings{ML:hscc07-full,
author = {S. Mitra and N. Lynch},
title = {Trace-based Semantics for Probabilistic Timed I/O Automata},
booktitle = {HSCC`07},
crossref = {HSCC2007},
year = {2007},
series = {LNCS},
volume = {4416}},
publisher = {Springer},
url = {http://people.csail.mit.edu/~mitras/research/PTIOA06-full.pdf}}
}
@inproceedings{GrosuM07,
author = {Radu Grosu and Sayan Mitra and Pei Ye and Emilia Entcheva and
I. V. Ramakrishnan and Scott A. Smolka},
title = {Learning Cycle-Linear Hybrid Automata for Excitable Cells.},
booktitle = {HSCC},
year = {2007},
PAGES = {245-258},
crossref = {HSCC2007}
}