To appear
Gregory Chockler, Seth Gilbert, Vincent C. Gramoli, Peter M.
Musial, and Alex A. Shvartsman. Reconfigurable Distributed Storage
for Dynamic Networks. To appear in Journal of Parallel and
Distributed Computing, 2008.
Alex Cornejo, Nancy Lynch. Connectivity Service for Mobile
Ad-Hoc Networks. To appear in Spatial Computing Workshop at 2nd IEEE
International Conference on Self-Adaptive and Self-Organizing Systems,
Venice, Italy, October 2008.
Seth Gilbert, Nancy Lynch, Sayan Mitra, and Tina Nolte. Self-Stabilizing Mobile Robot Formations with Virtual Nodes.
To appear in Proceedings of the Symposium on Stabilization, Safety and Security of Distributed Systems (SSS), December, 2008. .pdf
Seth Gilbert, Rachid Guerraoui, and Calvin Newport.
Of Malicious Motes and Suspicious Sensors: On the Efficiency of Malicious Interference in Wireless Networks. To appear in Theoretical Computer Science, 2008.
Idit Keidar. Group Communication.
Chapter in the Encyclopedia of Distributed Computing, Joseph Urban
and Partha Dasgupta, editors, Kluwer Academic Publishers. To be published.
ps,
ps.gz,
pdf
Daniel Liberzon, Nancy Lynch, and Sayan Mitra.
Verifying Average Dwell Time of Hybrid Systems. To appear in ACM Transactions in Embedded Computing Systems, 2008. .pdf
Shinya Umeno. Event order abstraction for parametric real-time system verification. To appear in International Conference on Embedded Software (EMSOFT 2008), Atlanta, Georgia, October 2008.
2008
R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, and R. Segala. Analyzing Security Protocol Using Time-Bounded Task-PIOAs. Journal of Discrete Event Dynamic Systems (DEDS), volume 18, number 1, March 2008. (Appears online February 2008). Springer. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Nancy Lynch, and Olivier Pereira.
Modeling Computational Security in Long-Lived Systems. CONCUR 2008: 19th International Conference on Concurrency Theory, Toronto, Canada, August 2008. .pdf.
Gregory Chockler, Seth Gilbert, and Nancy Lynch. Virtual Infrastructure for Collision-Prone Wireless Networks.
Proceedings of the 27th Symposium on Principles of Distributed Computing (PODC), 2008. .pdf
Gregory Chockler, Murat Demirbas, Seth Gilbert, Nancy Lynch, Calvin Newport, and Tina Nolte. Consensus and collision detectors in radio networks. Distributed Computing, 21(1):55-84, June 2008. Available online.
Shlomi Dolev, Seth Gilbert, Rachid Guerraoui, and Calvin Newport. Secure Communication over Radio Channels. Proceeding of the 27th
Symposium on Principles of Distributed Computing (PODC), Toronto, Canada, August 2008.
Rui Fan. Lower Bounds in Distributed Computing. Ph.D Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA, February 2008. .pdf
Seth Gilbert, Nancy Lynch, and Alex Shvartsman. RAMBO: A Robust, Reconfigurable Atomic Memory service for Dynamic Networks. Submitted for journal publication. .pdf
R. Grosu, X. Huang, N. Lynch, S.A. Smolka. Model Checking TIOA.
Technical Report CS-CL-08-02,Department of Computer Science, Stony Brook
University, Stony Brook, NY, USA, 2008.
Nancy Lynch, Laurent Michel, and Alexander Shvartsman. Tempo: A Toolkit for The Timed Input/Output Automata Formalism. First International Conference on Simulation Tools and Techniques for Communications, Networks, and Systems (SIMUTools 2008), Industrial Track: Simulation Works. Conference Proc. CD, paper 3105, 8 pages, Marseille, France, March 4-7, 2008. .pdf
Tina Nolte. Virtual Stationary Timed Automata for Mobile Networks. Ph.D Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA. To appear.
Mike Spindel. Simulation and Evaluation of the Reactive Virtual Node Layer.
Master of Engineering Thesis, Department of Electrical
Engineering and Computer Science, Massachusetts Institute of
Technology, Cambridge, MA, May 2008. .pdf
Shinya Umeno. Event order abstraction for parametric timed verification
. Second Workshop on Event-Based Semantics,
St. Louis MO, USA. April 21, 2008. .pdf
Jiang Wu, Nancy Griffeth, Nancy Lynch, Calvin Newport, Mike Spindel, and Ralph Droms. Using Virtual Infrastructure to Adapt Wireline Protocols to MANET. Submitted for publication.
2007
Paul Attie, Rachid Guerraoui, Petr Kouznetsov, Nancy Lynch, and Sergio Rajsbuam. The Impossibility of Boosting Distributed Service Resilience. Submitted for journal publication, Janauary, 2007. .pdf
Matthew D. Brown. Air Traffic Control Using Virtual Stationary Automata. Master of Engineering Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA, September 2007. .pdf
Matthew Brown, Seth Gilbert, Nancy Lynch, Calvin Newport, Tina
Nolte, and Michael Spindel. The Virtual Node Layer: A Programming
Abstraction for Wireless Sensor Networks. Proceedings of the
the International Workshop on Wireless Sensor Network Architecture
(WWSNA), Cambridge, MA, April, 2007. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Nancy Lynch, and Olivier Pereira.
Modeling Computational Security in Long-Lived Systems. Cryptology ePrint Archive Report 2007/406. .pdf.
Ran Canetti, Ling Cheung, Dilsun Kaynar, Nancy Lynch, and Olivier
Pereira. Compositional Security for Task-PIOAs. Proceedings of the 20th IEEE Computer Security Foundations
Symposium, Venice, Italy, July 2007. .pdf
Ran Canetti, Ling Cheung, Nancy Lynch, and Olivier Pereira.
On the Role of Scheduling in Simulation-Based Security.
7th International Workshop on Issues in the Theory of Security (WITS'07),
Braga, Portugal, March 2007. Also, ePrint Report 2007/12, Cryptology
ePrint archive, 2007. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Using Task-Structured
Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol.
ePrint Report 2005/452, Cryptology ePrint Archive, 2005. Also, Technical Report MIT-CSAIL-TR-2007-011, CSAIL, Massachusetts Institute of
Technology, Cambridge, MA, February 16, 2007. (Earlier version is
MIT-CSAIL-TR-2006-047). .pdf
Ling Cheung, Joseph A. Cooley, Roger Khazan, and Calvin Newport.
Collusion-Resistant Group Key Management Using Attribute-Based
Encryption. Proceedings of 1st International Workshop on
Group-Oriented Cryptographic Protocols, Wroclaw, Poland, July 2007. .pdf
Ling Cheung and Calvin Newport.
Provably Secure Ciphertext Policy ABE.
Proceedings of the 14th ACM Conference on Computer and Communications
Security (CCS), Alexandria, VA, October, 2007. Also, ePrint Report 2007/183, Cryptology ePrint archive, 2007. .pdf
Ling Cheung, Sayan Mitra and Olivier Pereira. Verifying Statistical
Zero Knowledge with Approximate Implementations. Cryptology ePrint Archive Report 2007/195. .pdf
Shlomi Dolev, Seth Gilbert, Rachid Guerraoui, and Calvin Newport. Gossiping in a Multi-Channel Radio Network: An Oblivious Approach to
Coping with Malicious Interference. Proceedings of the 21th International Symposium on Distributed
Computing (DISC), Lemesos, Cyprus, September, 2007. .pdf
Rui Fan, Ralph Droms, Nancy Griffeth, and Nancy Lynch. The DHCP
Failover Protocol: A Formal Perspective. 27th IFIP WG 6.1 International Conference on Formal Methods for
Networked and Distributed Systems (FORTE 2007), Tallinn, Estonia, June 26-29, 2007. .pdf
Seth Gilbert. Virtual Infrastructure for Wireless Ad Hoc
Networks. Ph.D Thesis, Department of Electrical Engineering and Computer Science,
Massachusetts Institute of Technology, Cambridge, MA 02139, 2007. .pdf
Radu Grosu, Sayan Mitra, Pei Ye, Scott Smolka, Emilia Entcheva, and I. O. Ramakrishnan. Learning cycle-linear hybrid automata of excitable cell models. In Hybrid Systems: Computation and Control (HSCC 07), volume 4416 of Lecture Notes in Computer Science, pages 245-258, April 2007. .pdf
Rachid Guerraoui, Maurice Herlihy, Petr Kouznetsov, Nancy Lynch, and Calvin Newport. On the weakest failure detector ever. Proceedings of the Twenty-Sixth Annual ACM Symposium on the Principles
of Distributed Computing (PODC), Portland, Oregon, August 2007. .pdf
Xavier Koegler (supervised by Nancy Lynch). Around the Tempo Toolset Userguide. March 20th-August 31st, 2007. .pdf
Carolos Livadas and Nancy A. Lynch. A Reliable Broadcast Scheme
for Sensor Networks. Technical Report MIT-LCS-TR-915, MIT Computer Science and
Artificial Intelligence Laboratory, Cambridge, MA, February 2007
(Revision of earlier version dated August 2003). .pdf
Nancy Lynch, Roberto Segala, and Frits Vaandrager.
Observing Branching Structure through Probabilistic Contexts. Siam
Journal on Computing, 37(4):977-1013, September 2007. .pdf
Sayan Mitra. A Verification Framework for Ordinary and
Probabilistic Hybrid Systems. Ph.D Thesis, Department of
Electrical Engineering and Computer Science, Massachusetts Institute
of Technology, Cambridge, MA, September 2007. .pdf
Sayan Mitra and Nancy Lynch. Proving approximate implementation relations for Probabilistic I/O Automata. Electronic Notes in Theoretical Computer Science, 174(8):71-93, 2007. .pdf
Sayan Mitra and Nancy Lynch. Trace-based semantics of Probabilistic timed I/O automata.
Hybrid Systems: Computation and Control (HSCC 2007), Pisa, Italy,
April 3-5, 2007, volume 4416 of Lecture Notes in Computer Science. Springer, 2007. .pdf
Tina Nolte and Nancy Lynch. Self-stabilization and Virtual Node Layer
Emulations. Proceedings of SSS 2007: Ninth International Symposium on
Stabilization, Safety, and Security of Distributed Systems, Paris, France,
November 2007. .pdf
Tina Nolte and Nancy Lynch. A Virtual Node-Based Tracking Algorithm for
Mobile Networks. International Conference on
Distributed Computing Systems (ICDCS 2007), Toronto, Canada, June, 2007. .pdf
Shinya Umeno and Nancy Lynch. Safety Verification of an Aircraft
Landing Protocol: A Refinement Approach. Hybrid Systems: Computation and Control (HSCC 2007), Pisa, Italy,
April 3-5, 2007, volume 4416 of Lecture Notes in Computer Science,
pages 557-572. .pdf
2006
Myla Archer, HongPing Lim, Nancy Lynch, Sayan Mitra and Shinya
Umeno. Specifying and Proving Properties of Timed I/O Automata in the TIOA
Toolkit. Fourth ACM-IEEE International
Conference on Formal Methods and Models for Codesign (MEMOCODE'06),
Napa Valley, California, July, 2006. .pdf
Paul Attie. On the Refinement of Liveness Properties of
Distributed Systems. Manuscript, 2006. pdf
Michael A. Bender, Jeremy T. Fineman, and Seth Gilbert.
Contention Resolution with Heterogeneous Job Sizes. Proceedings of the 14th Annual European Symposium on Algorithms,
September, 2006. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Time-bounded Task-PIOAs: A
Framework for Analyzing Security Protocols. 20th
International Symposium on Distributed Computing (DISC 2006),
Stockholm, Sweden, September 18-20, 2006. Invited paper. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Task-Structured Probabilistic
I/O Automata. Technical Report MIT-CSAIL-TR-2006-060, CSAIL,
Massachusetts Institute of Technology, Cambridge, MA, August, 2006..pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala.
Task-Structured Probabilistic I/O Automata.
Proceedings the 8th International Workshop on Discrete
Event Systems (WODES'06), Ann Arbor, Michigan, July, 2006. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Using Task-Structured Probabilistic
I/O Automata to Analyze Cryptographic Protocols. In V. Cortier,
S. Kremer, editors, Workshop on Formal and Computational
Cryptography - FCC 2006, pages 34--39, July 2006. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Using Task-Structured
Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol.
Technical Report MIT-CSAIL-TR-2006-047, CSAIL, Massachusetts Institute of
Technology, Cambridge, MA, June 19, 2006. (Latest version is
MIT-CSAIL-TR-2007-011). .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Using Probabilistic I/O
Automata to Analyze an Oblivious Transfer Protocol. Technical
Report MIT-CSAIL-TR-2006-046, CSAIL, Massachusetts Institute of
Technology, Cambridge, MA, January 10, 2006. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Task-Structured Probabilistic
I/O Automata. Technical Report MIT-CSAIL-TR-2006-023, CSAIL,
Massachusetts Institute of Technology, Cambridge, MA, March, 2006. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Using Task-Structured
Probabilistic I/O Automata to Analyze an Oblivious Transfer
Protocol. Technical Report MIT-CSAIL-TR-2006-019, CSAIL, Massachusetts Institute of
Technology, Cambridge, MA, March, 2006. .pdf
Ling Cheung, Nancy Lynch, Roberto Segala, and Frits Vaandrager.
Switched Probabilistic PIOA: Parallel Composition via
Distributed Scheduling. Theoretical Computer Science, volume 365, issues 1-2, pages 83-108, 10 November 2006.
.pdf
Gregory Chockler, Seth Gilbert, and Boaz Patt-Shamir. Communication-Efficient
Probabilistic Quorum Systems. Proceedings of the IEEE International
Workshop on Foundations and Algorithms for Wireless Networking (FAWN),
March 29-31, 2006. .pdf
Constantinos Djouvas, Nancy D. Griffeth, and Nancy A. Lynch.
Testing Self-Similar Networks MBT 2006: Second Workshop on
Model Based Testing, Electronic Notes in Theoretical Computer
Science, issue 4, volume 164, March 2006. .pdf
Rui Fan and Nancy Lynch. Gradient Clock Synchronization.
Distributed Computing, volume 18, number 4, pages 255-266,
March, 2006. .pdf.
Rui Fan and Nancy Lynch. An Ω (n log n) Lower Bound on
the Cost of Mutual Exclusion. Proceedings of the
Twenty-Fifth Annual Symposium on Principles of Distributed Computing
(PODC'06), Denver, Colorado, July 2006. .pdf
Seth Gilbert, Rachid Guerraoui, and Calvin Newport. Of
Malicious Motes and Suspicious Sensors: On the Efficiency of Malicious
Interference in Wireless Networks. Proceedings
of the 10th International Conference On Principles Of Distributed
Systems (OPODIS), Bordeaux, France, December 12-15, 2006.
Seth Gilbert, Rachid Guerraoui, and Calvin Newport. Of
Malicious Motes and Suspicious Sensors. Technical Report
MIT-CSAIL-TR-2006-026, CSAIL, Massachusetts Institute of Technology,
Cambridge, MA, April 2006. .pdf
Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager.
The Theory of Timed I/O Automata.Synthesis Lectures on Computer Science, Morgan Claypool
Publishers, 2006. Revised and shortened version
of Technical Report MIT-LCS-TR-917a (from 2004). .pdf
K. Konwar, P.M. Musial, N.C. Nicolau, and A.A. Shvartsman.
Implementing Atomic Data through Indirect Learning in Dynamic
Networks. Technical Report MIT-CSAIL-TR-2006-070, Computer
Science and Artificial Intelligence Laboratory, Massahusetts instute
of Technology, Cambridge, MA, October 2006. .pdf
Matthew Lepinski, David Liben-Nowell, Seth Gilbert, and April Rasala
Lehman. Playing Games in Many Possible Worlds. Proceedings
of the Seventh ACM Conference on Electronic Commerce, June, 2006.
.ps
Sayan Mitra and Nancy Lynch. Approximate simulations for
task-structured probabilistic I/O automata.
LICS workshop on Probabilistic Automata and Logics
(PAul06), Seattle, WA, August 2006. .pdf
Sayan Mitra, Daniel Liberzon, and Nancy Lynch. Verifying average
dwell time by solving optimization problems. In Ashish Tiwari and
Joao P. Hespanha, editors, Hybrid Systems: Computation and
Control (HSCC 06) Santa Barbara, CA, March 2006, volume 3927
of Lecture Notes in Computer Science, pages 476-490, 2006. Springer. .pdf
Calvin Newport. Consensus and Collision Detectors in Wireless
Ad Hoc Networks. Masters Thesis, MIT Department of Electrical
Engineering and Computer Science, Cambridge, MA, June 2006. .ps
Shinya Umeno and Nancy Lynch.
Proving safety properties of an aircraft landing protocol
using I/O Automata and the PVS theorem prover: a case study.
FM 2006: Formal Methods,
International Symposium of Formal Methods Europe,
Hamilton, Ontario Canada, August, 2006. Volume 4085 of
Lecture Notes in Computer Science, pages 64-80, Springer,
2006. .pdf
Shinya Umeno. Proving safety properties of an aircraft landing
protocol using timed anduntimed I/O automata: a case study.
Masters Thesis, Department of Electrical Engineering and Computer
Science, Massachusetts Institute of Technology, Cambridge, MA, October
2006. .pdf
2005
Paul Attie and Hana Chockler.
Efficiently Verifiable Conditions for Deadlock-freedom of
Large Concurrent Programs. Proceedings of the Sixth
International Conference on Verification, Model Checking and Abstract
Interpretation, Paris, France, January 2005. .pdf
Paul Attie, Rachid Guerraoui, Petr Kouznetsov, Nancy Lynch, and Sergio
Rajsbaum. The Impossibility of Boosting Distributed Service
Resilience. 25th IEEE International Conference on
Distributed Computing Systems (ICDCS 2005), Columbus, OH, pages
39-48, June 6-10, 2005. .pdf
Paul Attie, Rachid Guerraoui, Petr Kouznetsov, Nancy Lynch, and Sergio
Rajsbaum. Impossibility of boosting distributed service resilience.
Technical Report MIT-LCS-TR-982, Computer Science and Artificial
Intelligence Laboratory, Massachusetts Institute of Technology,
Cambridge, MA, February 2005. .ps
Michael Bender, Jeremy Fineman, Seth Gilbert, and Bradley Kuszmaul.
Concurrent Cache-Oblivious B-Trees. 17th ACM Symposium on Parallelism in Algorithms
and Architectures (SPAA 2005), Las Vegas, Nevada, July 2005. .pdf
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov,
Nancy Lynch, Olivier Pereira, and Roberto Segala.
Using Probabilistic I/O Automata to Analyze an Oblivious Transfer
Protocol.ePrint Report 2005/452, Cryptology ePrint Archive, 2005.
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, and Roberto Segala. Using Probabilistic I/O Automata
to Improve the Analysis of Cryptographic Protocols. In ERCIM
News, 63: 40-41, October 2005. .html
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy
Lynch, Olivier Pereira, and Roberto Segala. Using Probabilistic I/O
Automata to Analyze an Oblivious Transfer Protocol. Technical
Report CSAIL-TR-2005-055, MIT CSAIL, Cambridge, MA, August 2005. .pdf
Gregory Chockler and Dahlia Malkhi.
Active Disk Paxos with infinitely many processes.
Distributed Computing, volume 18, number 1, pages 73-84,
July 2005. .ps
Gregory Chockler, Nancy Lynch, Sayan Mitras, and Joshua
Tauber. Proving Atomicity: An Assertional Approach DISC 2005: 19th International Symposium on Distributed Computing,
Cracow, Poland, September 2005. .pdf
G. Chockler, M. Demirbas, S. Gilbert, and C. Newport. A Middleware Framework for Robust Applications in Wireless Ad Hoc
Networks. Allerton Conference 2005: Forty-Third Annual Allerton Conference on
Communication, Control, and Computing, September 2005. .pdf
Gregory Chockler, Murat Demirbas, Seth Gilbert, Nancy Lynch, Calvin
Newport, and Tina Nolte. Reconciling the Theory and Practice of (Un)Reliable Wireless Broadcast.
Proceedings of the 4th International
Workshop on Assurance in Distributed Systems and Networks (ADSN 2005),
June 6, 2005, Columbus, Ohio, USA. .pdf
Gregory Chockler, Murat Demirbas, Seth Gilbert, Calvin Newport, and Tina
Nolte. Consensus and Collision Detectors in Wireless Ad Hoc
Networks. Twenty-Fourth Annual ACM
SIGACT-SIGOPS Symposium on Principles of Distributed Computing
(PODC 2005), Las Vegas, Nevada, pages 197-206, July 2005. .pdf
Gregory Chockler, Seth Gilbert, Vincent Gramoli, Peter
Musial, and Alexander Shvartsman. Reconfigurable Distributed
Storage for Dynamic Networks. 9th International Conference on
Principles of Distributed Systems (OPODIS 2005), Pisa, Italy,
December 12-14, 2005. .pdf
Gregory Chockler, Nancy Lynch, Sayan Mitra, and Joshua
Tauber. Proving Atomicity: An Assertional Approach. Technical
Report MIT-CSAIL-TR-2005-048 (and MIT-LCS-TR-995), MIT CSAIL, Cambridge, MA, July 2005. .pdf
Shlomi Dolev, Limor Lahiani, Nancy Lynch, and Tina Nolte.
Self-Stabilizing Mobile Node Location Management and Message Routing.
Self-Stabilizing Systems: Seventh International Symposium on Self
Stabilizing Systems (SSS 2005), Barcelona, Spain, October 26-27,
2005, volume 3764 of {\em Lecture Notes in Computer Science}, pages 96-112, 2005. Springer. Also, Technical Report MIT-LCS-TR-999, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, MA, August 2005. .pdf
Shlomi Dolev, Seth Gilbert, Limor Lahiani, Nancy Lynch, and Tina Nolte.
Timed Virtual Stationary Automata for Mobile Networks.
Principles of Distributed systems: 9th International Conference on
Principles of Distributed Systems (OPODIS 2005), volume 3974 of Lecture Notes in Computer Science, pages 130-145, 2006, Springer. Also, Technical Report MIT-LCS-TR-979a, MIT CSAIL, Cambridge, MA 02139, August 2005.
.ps
Shlomi Dolev, Seth Gilbert, Limor Lahiani, Nancy Lynch, and Tina Nolte.
Timed Virtual Stationary Automata for Mobile Networks. Allerton Conference 2005: Forty-Third Annual Allerton Conference on
Communication, Control, and Computing, September 2005. Invited
paper. .pdf
Shlomi Dolev, Seth Gilbert, Nancy A. Lynch, Alex A. Shvartsman, and
Jennifer L. Welch. GeoQuorums: Implementing Atomic Memory in
Mobile Ad Hoc Networks. Distributed
Computing, Special Issue DISC03, 18(2):125-155, 2005.
Also, Technical Report MIT-LCS-TR-900a,
CSAIL, Massachusetts Institute of Technology, Cambridge, MA, 2004. .ps
Shlomi Dolev, Seth Gilbert, Elad Schiller, Alex A. Shvartsman, and
Jennifer Welch. Autonomous Virtual Mobile Nodes.
DIAL-M-POMC 2005: Third Annual ACM/SIGMOBILE International Workshop on
Foundation of Mobile Computing, Cologne, Germany, September 2,
2005. .pdf
Shlomi Dolev, Seth Gilbert, Elad Schiller, Alex Shvartsman, Jennifer
Welch. Brief Announcement: Autonomous Virtual Mobile Nodes.
17th ACM Symposium on Parallelism in Algorithms
and Architectures (SPAA 2005), Las Vegas, Nevada, July 2005. .ps
Shlomi Dolev, Limor Lahiani, Seth Gilbert, Nancy Lynch, Tina Nolte.
Brief Announcement: Virtual Stationary Automata for Mobile Networks.
Proceedings of the 24th Annual ACM Symposium on
Principles of Distributed Computing (PODC'05), Las Vegas, Nevada,
July, 2005. .pdf
Shlomi Dolev, Seth Gilbert, Limor Lahiani, Nancy Lynch, and Tina
Nolte. Timed Virtual Stationary Automata for Mobile Networks.
Techncial Report MIT-LCS-TR-979a, MIT CSAIL, Cambridge, MA, August
2005. .ps
Shlomi Dolev, Seth Gilbert, Elad Schiller, Alex Shvartsman, and
Jennifer Welch. Autonomous Virtual Mobile Nodes. Technical Report
MIT-LCS-TR-992, MIT CSAIL, Cambridge, MA, June 2005. .pdf
Shlomi Dolev, Seth Gilbert, Limor Lahiani, Nancy Lynch,
and Tina Nolte.
Virtual Stationary Automata for Mobile Networks (Extended
Abstract) Technical Report MIT-LCS-TR-979, MIT CSAIL, Cambridge,
MA 02139, January 2005. .ps
Shlomi Dolev, Limor Lahiani, Nancy Lynch, and Tina Nolte.
Self-Stabilizing Mobile Node Location Management and Message Routing.
Technical Report MIT-LCS-TR-999, MIT Computer Science and Artificial
Intelligence Laboratory, Cambridge, MA, August 2005. .ps
Stephen Garland. TIOA User Guide and Reference Manual. September 15,
2005. .pdf
Stephen Garland, Dilsun Kaynar, Nancy Lynch, Joshua Tauber, and
Mandana Vaziri. TIOA Tutorial. May 22, 2005. .pdf
Dilsun Kaynar, Nancy Lynch, Sayan Mitra, and Stephen Garland.
The TIOA Language. Version 0.21, May 22, 2005. .pdf
Ben Leong, Sayan Mitra, and Barbara Liskov. Path vector face routing:
Geographic routing with local face information.
Proceedings of 13th IEEE International Conference
on Network Protocols (ICNP'05 ), November
6-9, 2005, Boston, Massachusetts, USA. .pdf
Hongping Lim, Dilsun Kaynar, Nancy Lynch, and Sayan Mitra. Translating
timed I/O automata specifications for theorem proving in PVS.
Proceedings of International Conference on Formal
Modelling and Analysis of Timed Systems (FORMATS'05), Uppsala,
Sweden, September 26 - 28, 2005. .pdf
Nancy Lynch. A Three-Level
Analysis of a Simple Acceleration Maneuver, with Uncertainties. In Aurel Cornell and Dan Ionescu, editors, Real-Time
Systems: Modeling, Design, and Applications, volume 8 of AMAST
Series in Computing, World Scientific Publishing Company, 2005. Abstract
and Postscript
Nancy Lynch, Sayan Mitra, and Tina Nolte. Motion coordination
using virtual nodes. Technical Report MIT-LCS-TR-986, MIT CSAIL, Cambridge, MA,
April 2005. .pdf
Nancy Lynch, Sayan Mitra, and Tina Nolte. Motion Coordination Using
Virtual Nodes. CDC-ECC 2005: Forty-Fourth IEEE Conference on
Decision and Control and European Control Conference, Seville,
Spain, December 2005. Invited paper. .pdf
Sayan Mitra and Myla Archer. PVS Strategies for proving abstraction
properties automata.
In Electronic Notes in Theoretical Computer Science, volume 125(2),
2005, pages 45-65. .ps
Sayan Mitra and Daniel Liberzon.
Stability of Hybrid Automata with Average Dwell Time: An Invariant
Approach. Proceedings of the 43rd Conference on
Decision and Control, Paradise Island, Bahamas, December, 2004.
.ps
Athicha Muthitacharoen, Seth Gilbert, and Robert Morris.
Etna: A Fault-tolerant Algorithm for Atomic Mutable DHT Data.
Technical Report MIT-CSAIL-TR-2005-044, MIT CSAIL, Cambridge, MA, June
2005. .pdf
Joshua A. Tauber. Verifiable Compilation of I/O Automata
without Global Synchronization. Ph.D Thesis,
Department of Electrical Engineering and Computer Science,
Massachusetts Institute of Technology, Cambridge, MA 02139, February,
2005. .pdf
2004
Ittai Abraham, Gregory Chockler, Idit Keidar and Dahlia Malkhi.
Byzantine Disk Paxos: Optimal Resilience with Byzantine Shared
Memory. Proceedings of the 23rd Annual ACM
SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC
2004), St. John's, Newfoundland, Canada, pages 226-235, July 2004.
© ACM, (2004). This is the author's version of the work. It is posted
here by permission of ACM for your personal use. Not for
redistribution. The definitive version was published in the
Proceedings of the Twenty-Third Annual ACM SIGACT-SIGOPS Symposium on
Principles of Distributed Computing (PODC 2004). .pdf
P.C. Attie, A. Arora, and E.A. Emerson.
ACM Transactions on Programming Languages and Systems (TOPLAS),
vol. 26, no. 1, pp 125-185, January 2004.
Extended abstract appears in ACM Symposium on the Principles of
Distributed Computing (PODC) 1998. .pdf
Jacob Beal and Seth Gilbert. RamboNodes for the Metropolitan Ad
Hoc Network. Proceedings of the Workshop on Dependability in
Wireless Ad Hoc Networks and Sensor Networks, part of the
International Conference on Dependable Systems and Networks,
Florence, Italy, June-July, 2004. .ps
Also, AI Memo: AIM-2003-027.
Michael A. Bender, Jeremy T. Fineman, Seth Gilbert, Charles E. Leiserson.
On-the-Fly Maintenance of Series-Parallel Relationships in Fork-Join
Multithreaded Programs. Sixteenth ACM
Symposium on Parallelism in Algorithms and Architectures (SPAA 2004), Barcelona,
Spain, pages 133-144, June 27-30, 2004..ps
Ling Cheung, Nancy Lynch, Roberto Segala, and Frits Vaandrager.
Switched Probabilistic I/O Automata. In Z. Liu and K. Araki,
editors, Proceedings of the First International Colloquium on Theoretical
Aspects of Computing (ICTAC2004), Guiyang, China, September 2004,
volume 3407 of Lecture Notes in Computer Science, pages
494-510, Springer-Verlag, 2005. .pdf
Ling Cheung, Nancy Lynch, Roberto Segala, and Frits Vaandrager.
Switched Probabilistic I/O Automata. Nijmegen Institute for
Computing and Information Sciences (NIII) Technical Report NIII-R0437,
Catholic University of Nijmegen, Nijmegen, The Netherlands, September 2004.
.ps
G. Chockler and D. Malkhi.
Light-Weight Leases for Storage-Centric Coordination.
Technical Report MIT-LCS-TR-934, MIT Laboratory for Computer Science,
January, 2004. Revised April 2004. .ps
Gregory Chockler, Idit Keidar and Dahlia Malkhi. Optimal Resilience Wait-Free Storage from Byzantine Components: Inherent
Costs and Solutions. FuDiCo II: S.O.S. Survivability: Obstacles and Solutions. 2nd Bertinoro
Workshop on Future Directions in Distributed Computing, 23-25 June 2004
University of Bologna Residential Center Bertinoro (Forli), Italy..pdf
Murat Demirbas, Anish Arora, Tina Nolte, and Nancy Lynch. A
Hierarchy-based Fault-local Stabilizing Algorithm for Tracking in
Sensor Networks. In Teruo Higashino,
editor, Principles of Distributed Systems: OPODIS 2004: 8th
International Conference on Principles of Distributed Systems, Grenoble, France, December 15-17, 2004,
volume 3544 of Lecture Notes in Computer Science, pages 299-315,
2005. Springer. .pdf.
Murat Demirbas, Anish Arora, Tina Nolte, and Nancy Lynch. Brief
Announcement: STALK: A Self-Stabilizing Hierarchical Tracking Service
for Sensor Networks. Proceedings of the 23rd Annual ACM SIGACT-SIGOPS
Symposium on Principles of Distributed Computing (PODC 2004),
St. John's, Newfoundland, Canada, page 378, July 25-28, 2004. .ps
Shlomi Dolev, Seth Gilbert, Nancy A. Lynch, Elad Schiller, Alex
A. Shvartsman, and Jennifer L. Welch. Virtual Mobile Nodes for
Mobile Ad Hoc Networks. 18th International
Symposium on Distributed Computing (DISC04), Trippenhuis, Amsterdam, the
Netherlands, October 4-7, 2004. .ps
Also, in Rachid
Guerraoui, editor, volume 3274 of Lecture Notes in
Computer Science, Springer-Verlag, December 2004.
Shlomi Dolev, Seth Gilbert, Nancy Lynch, Elad Schiller, Alex
Shvartsman, Jennifer Welch. Brief Announcement: Virtual Mobile
Nodes for Mobile Ad Hoc Networks. Proceedings of the 23rd Annual ACM SIGACT-SIGOPS
Symposium on Principles of Distributed Computing (PODC 2004),
St. John's, Newfoundland, Canada, page 385, July 25-28, 2004. .pdf
Also, Technical
Report MIT-LCS-TR-937, MIT CSAIL, Cambridge, MA, 2004.
Shlomi Dolev, Seth Gilbert, Nancy A. Lynch, Alex A. Shvartsman, and
Jennifer L. Welch. GeoQuorums: Implementing Atomic Memory in Ad
Hoc Networks. Technical Report MIT-LCS-TR-900a,
CSAIL, Massachusetts Institute of Technology, Cambridge, MA, 2004. .ps
Rui Fan, Indraneel Chakraborty, and Nancy Lynch. Clock
Synchronization for Wireless Networks. In Teruo Higashino,
editor, Principles of
Distributed Systems: OPODIS 2004: 8th International Conference on Principles of
Distributed Systems, Grenoble, France, December 15-17, 2004,
volume 3544 of Lecture Notes in Computer Science, pages 400-414,
2005. Springer. .ps
Chryssis Georgiou, Peter M. Musial, and Alexander A. Shvartsman.
Long-Lived Rambo: Trading Knowledge for Communication.
Rastislav Kralovic, Ondrej Sykora (Eds.): Structural Information and
Communication Complexity, 11th International Colloquium, SIROCCO
2004, Smolenice Castle, Slowakia, June 21-23, 2004, volume 3104 of
Lecture Notes in Computer Science, pages 185-196, Springer 2004.
Chryssis Georgiou, Peter M. Musial, and Alexander A. Shvartsman.
Long-Lived Rambo: Trading Knowledge for Communication.
Technical Report MIT-LCS-TR-943, MIT CSAIL, Cambridge, MA, April
2004. .ps
Rui Fan and Nancy Lynch. Gradient Clock Synchronization.
Proceedings of the Twenty-Third Annual ACM SIGACT-SIGOPS
Symposium on Principles of Distributed Computing (PODC 2004)), St. John's,
Newfoundland, Canada, pages 320-327, July 25-58, 2004. Best
Student Paper Award. .ps
Stephen Garland, Nancy Lynch, Joshua Tauber, and Mandana Vaziri.
IOA User Guide and Reference Manual.
Technical Report MIT-LCS-TR-961, MIT CSAIL, July 2004.
Ch. Georgiou, A. Russell and A. Shvartsman.
The Complexity of Synchronous Iterative Do-All with Crashes.
Distributed Computing, Volume 17, No. 1, pages 47-63, 2004.
.pdf
Chryssis Georgiou, Panayiotis Mavrommatis and Joshua A.
Tauber. Implementing Asynchronous Distributed Systems Using the IOA
Toolkit. MIT CSAIL Technical Report MIT-LCS-TR-966, Cambridge,
MA, November 2004. .ps
Seth Gilbert and Gregory Malewicz. The Quorum Deployment Problem.
OPODIS 2004: 8th International Conference on
Principles of Distributed Systems, Grenoble, France, December
15-17, 2004. .ps
Also, full version in MIT CSAIL Technical Report MIT-LCS-TR-972,
October 2004. .ps
Seth Gilbert, Nancy Lynch, and Alex Shvartsman. RAMBO II:
Implementing atomic memory in dynamic networks, using an aggressive
reconfiguration strategy. Technical Report MIT-CSAIL-TR-890, CSAIL,
Massachusetts Institute Technology, Cambridge, MA, 2004. .ps
Dilsun Kaynar, Nancy Lynch, Sayan Mitra, Christine
Robson. Design for TIOA Modeling Language. Manuscript in
progress, 2004.
.html
Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager.
The Theory of Timed I/O Automata. Technical Report
MIT-LCS-TR-917a, MIT Laboratory for Computer Science, Cambridge, MA,
November, 2004. .ps
Revised version to appear in Synthesis Lectures on Computer
Science, Morgan Claypool Publishers, November 2005.
Dilsun K. Kaynar and Nancy A. Lynch. Decomposing Verification
of Timed I/O Automata. Formal Techniques, Modelling and
Analysis of Timed and Fault Tolerant Systems: Joint International
Conferences on Formal Modeling and Analysis of Timed Systems, FORMATS
2004, and Format Technicques in Real-Time and Fault-Tolerant Systems,
FTRTFT 2004, Grenoble, France, September 22-24, 2004. Volume 3253 of
Lecture Notes in Computer Science, pages 84-101, Springer-Verlag, 2004. .ps
Also, on the Springer website.
Dilsun Kaynar, Nancy Lynch, and Sayan Mitra.
Specifying and Proving Timing Properties with TIOA Tools.
25th IEEE International Real-Time Systems
Symposium, Work in Progress Session (RTSS 2004 WIP), December 5-8
2004, Lisbon, Portugal. .ps
Carl Livadas and Idit Keidar.
Caching-Enhanced Scalable Reliable Multicast.
International Conference on Dependable Systems
and Networks (DSN), June-July 2004. .ps
Nancy Lynch and Ion Stoica. MultiChord: A resilient namespace management
algorithm. Technical Memo MIT-LCS-TR-936, CSAIL,
Massachusetts Institute of Technology, Cambridge, MA 2004. .ps
Nancy Lynch, Roberto Segala, and Frits Vaandrager.
Compositionality for Probabilistic Automata.
Technical Report MIT-LCS-TR-907, Computer Science and Artificial Intelligence
Laboratory, Massachusetts Institute of Technology, Cambridge, MA,
November 2004. .ps
Catherine Matlon. A specification and verification of
Intermittent Global Order Broadcast. Master of Engineering in
Electrical Engineering and Computer Science, Massachusetts Institute
of Technology, Cambridge, MA, May 2004.
Sayan Mitra and Myla Archer.
Reusable PVS Proof Strategies for Proving Abstraction Properties of
I/O Automata. STRATEGIES 2004, IJCAR Workshop on Strategies in
Automated Deduction, Cork Ireland, July 2004. .ps
Sayan Mitra and Jesse Rabek.
Energy Efficient Connected Clusters for Mobile Ad Hoc Networks.
MED-HOC-NET 2004, Third Annual Mediterranean
Ad Hoc Networking Workshop, Bodrum, Turkey, June 2004. .ps
P.M. Musial and A.A. Shvartsman. Implementing a Reconfigurable
Atomic Memory Service for Dynamic Networks. In Proceedings
of the 18'th International Parallel and Distributed Processing Symposium
(IPDPS'04) --- FTPDS WS, Santa Fe, New Mexico, pages 208-215, April, 2004. .pdf
Christine Margaret Robson. TIOA and UPPAAL.
Masters of Engineering Thesis, MIT Department of Electrical
Engineering and Computer Science, Cambridge, MA, May 2004. .ps
A. Russell and A. Shvartsman.
Distributed Computation Meets Design Theory: Local Scheduling for
Disconnected Cooperation. Current Trends in Theoretical Computer Science:
The Challenge of the New Century, vol. 1: Algorithms and Complexity,
pp. 315-336, World Scientific, 2004. .ps
Joshua A. Tauber and Nancy A. Lynch and Michael J. Tsai.
Compiling IOA without Global Synchronization.
Proceedings of the 3rd IEEE International Symposium on
Network Computing and Applications (IEEE NCA04), Cambridge, MA, August
2004. .pdf
Joshua A. Tauber and Stephen J. Garland. Definition and
Expansion of Composite Automata in IOA. MIT CSAIL Technical
Report MIT-LCS-TR-959, July 2004. .pdf
Mandana Vaziri, Joshua A. Tauber, Michael J. Tsai, and Nancy Lynch.
Systematic Removal of Nondeterminism for Code Generation in I/O
Automata. MIT CSAIL Technical Report MIT-LCS-TR-960,
July 2004. .ps
2003
Paul C. Attie. On the Implementation Complexity of Specifications of
Concurrent Programs. Distributed Computing (DISC 2003: 17th International Symposium on
Distributed Computing, Sorrento, Italy, October 2003), volume 2848 of
Lecture Notes in Computer Science, pages 151-165, Springer-Verlag, 2003. .pdf
Paul C. Attie and Nancy A. Lynch. Dynamic Input/Output Automata: a
Formal Model for Dynamic Systems. Technical Report
MIT-LCS-TR-902, MIT Laboratory for Computer Science, Cambridge, MA,
02139, July 2003 and Technical Report, College of
Computer Science, Northeastern University, July 2003. Postscript
Omar Bakr. Performance Evaluation of Distributed Algorithms over the
Internet. Master of Engineering in Electrical Engineering and
Computer Science, Massachusetts Institute of Technology, Cambridge,
MA, February 2003. .ps
M. Demirbas, A. Arora, T. Nolte, and N. Lynch.
Stalk: A Self-Stabilizing Hierarchical Tracking Service
for Sensor Networks Technical Report OSU-CISRC-4/03-TR19,
Ohio State University, April 2003. .pdf
Shlomi Dolev, Seth Gilbert, Nancy Lynch, Alex Shvartsman, and Jennifer
Welch. GeoQuorums: Implementing Atomic Memory in Ad Hoc Networks.
In Faith Fich, editor, Distributed Computing (DISC 2003: 17th International Symposium on Distributed
Computing, Sorrento, Italy, October, 2003), volume 2848 of Lecture
Notes in Computer Science, pages 306-320, Springer-Verlag, 2003. .pdf
Shlomi Dolev, Seth Gilbert, Nancy Lynch, Alex Shvartsman, and Jennifer Welch.
GeoQuorums: Implementing atomic memory in ad hoc networks.
Technical Report MIT-LCS-TR-900, MIT Laboratory for Computer Science,
Cambridge, MA, 02139, 2003. .ps
Rui Fan and Nancy Lynch. Efficient Replication of Large Data
Objects. Distributed Computing (DISC 2003: 17th International Symposium on Distributed
Computing, Sorrento, Italy, October, 2003), volume 2848 of Lecture
Notes in Computer Science, pages 75-91, Springer-Verlag, 2003. .pdf
Rui Fan. Efficient Replication of Large Data Objects. Masters
Thesis, MIT Department of Electrical Engineering and Computer Science,
Cambridge, MA, February 2003. .ps
Rui Fan and Nancy Lynch. Efficient replication of large data
objects. Proceedings of the Twenty-Second Annual ACM Symposium on
Principles of Distributed Computing, Boston, Massachusetts, page
335, July 2003. .pdf
Rui Fan and Sayan Mitra. General fault tolerant data structures.
Manuscript, 2003.
Ch. Georgiou. Cooperative Distributed Computing in the
Presence of Quantified Adversity. Ph.D. thesis, University of
Connecticut, 2003. .ps
Ch. Georgiou, A. Russell and A. Shvartsman. Work-Competitive
Scheduling for Cooperative Computing with Dynamic Groups.
The Thirty-Fifth Annual ACM Symposium on Theory of Computing
(STOC'2003), pages 251-258, San Diego, CA, June 2003. .pdf
Ch. Georgiou and A.A. Shvartsman. Cooperative Computing with
Fragmentable and Mergeable Groups. Journal of Discrete
Algorithms, volume 1 (2), pp. 211-235, 2003..ps
Seth Gilbert. RAMBO II: Rapidly Reconfigurable Atomic Memory for
Dynamic Networks. Masters Thesis, Department of Electrical Engineering and Computer
Science, Massachusetts Institute of Technology, Cambridge, MA, August
2003. .ps
Seth Gilbert, Nancy Lynch, and Alex Shvartsman.
RAMBO II: Rapidly Reconfigurable Atomic Memory for Dynamic
Networks.
Proceedings of the International Conference on Dependable Systems
and Networks (DSN), San Francisco, CA, pages 259-268, June 22nd - 25th, 2003. .ps
Vida Uyen Ha. Verification of an Attitude Control System. Bachelor
of Science and Master of Engineering, Department of Electrical
Engineering and Computer Science, Massachusetts Institute of
Technology, Cambridge, MA, May 2003. .doc
Mohammad Taghi Hajiaghayi, Nicole Immorlica, and Vahab S. Mirrokni.
Power optimization in fault-tolerant topology control algorithms
for wireless multi-hop networks. MOBICOM 2003: Proceedings of
the Ninth Annual ACM International Conference on Mobile Computing and
Networking, pages 300-312, San Diego, CA, September 2003. .ps
Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager.
Timed I/O Automata: A Mathematical Framework for Modeling and
Analyzing Real-Time Systems. RTSS 2003: The 24th
IEEE International Real-Time Systems Symposium, Cancun, Mexico, pages
166-177, December, 2003. IEEE Computer Society. .ps
(Full version available as Technical Report MIT/LCS/TR-917.)
Dilsun K. Kaynar, Nancy Lynch, Roberto Segala, and Frits Vaandrager.
The Theory of Timed I/O Automata. Technical Report
MIT-LCS-TR-917, MIT Laboratory for Computer Science, Cambridge, MA, 2003. .ps
Idit Keidar and Sergio Rajsbaum.
A Simple Proof of the Uniform Consensus Synchronous Lower Bound.
Information Processing Letters (IPL), 85(1):47-52, January
2003. .pdf
Roger Khazan and Nancy Lynch. An Algorithm for an
Intermittently Atomic Data Service Based on Group Communication.
Proceedings of the International Workshop on Large-Scale Group Communication,
Florence, Italy, pages 25-30, October 2003. .pdf
Carolos Livadas. Formally Modeling, Analyzing, and Designing Network
Protocols---A Case Study on Retransmission-Based Reliable Multicast --Protocols. Ph.D Thesis, Department of Electrical Engineering and
Computer Science, Massachusetts Institute of Technology, Cambridge,
MA, July 2003. .ps
Nancy Lynch. Some Perspectives on PODC. Distributed
Computing, 16(1):71-74, 2003. .pdf
Nancy Lynch. Working with Mike on Distributed Computing Theory,
1978-1992.Proceedings of the Twenty-Second Annual ACM Symposium on
Principles of Distributed Computing (PODC'03), page 11, Boston, MA, July
2003.
.pdf
Nancy Lynch, Roberto Segala, and Frits Vaandrager.
Compositionality for Probabilistic Automata. In
Roberto Amadio and Denis Lugiez, editors, CONCUR 2003 - Concurrency
Theory (14th International Conference on Concurrency Theory, Marseille,
France, September, 2003), volume 2761 of Lecture Notes in Computer Science,
pages 208-221, Springer-Verlag, 2003. .pdf
Also, long
version as Technical Report MIT-LCS-TR-907, MIT Laboratory for
Computer Science, Cambridge, MA.
Nancy Lynch, Roberto Segala, and Frits Vaandraager. Hybrid I/O Automata.
Information
and Computation, 185(1):105-157, August 2003. Also, Technical
Report MIT-LCS-TR-827d, MIT Laboratory
for Computer Science, Cambridge, MA 02139, January 13, 2003.
G. Malewicz. Distributed Scheduling for Disconnected
Cooperation. Ph.D. thesis, University of Connecticut, 2003. .pdf
Sayan Mitra, Yong Wang, Nancy Lynch, and Eric Feron.
Safety Verification of Model Helicopter Controller using Hybrid
Input/Output Automata. O. Maler, A. Pnueli, editors, Hybrid
Systems: Computation and Control (6th International Workshop,
HSCC'03, Prague, the Czech Republic April 3-5, 2003), volume 2623 of
Lecture Notes in Computer Science, pages 343-358, Springer-Verlag, 2003..ps (Long version below).
Sayan Mitra, Yong Wang, Nancy Lynch, and Eric Feron.
Application of Hybrid I/O Automata in Safety Verification of
Pitch Controller for Model Helicopter System.
Technical Report MIT-LCS-TR-880, MIT Laboratory for Computer Science,
Cambridge, MA 02139, January 2003. .ps
Sayan Mitra and Myla Archer.
Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata.
In STRATA 2003, Design and Application of Strategies/Tactics in
Higher Order Logics, Rome, Italy, September, 2003. .ps
M. Momenzadeh. Emulating Shared-Memory Do-All in Asynchronous
Message Passing Systems.
Masters thesis, University of Connecticut, 2003.
Toh Ne Win. Theorem-Proving Distributed Algorithms with Dynamic
Analysis. Master of Engineering in Computer Science and Engineering,
MIT Department of Electrical Engineering, Cambridge, MA, May 2003. .ps
Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun K. Kaynar,
and Nancy Lynch. Using simulated execution in verifying
distributed algorithms. In L.D. Zuck, P.C. Attie, A. Cortesi,
S. Mukhopadhyay, editors, Verification, Model Checking, and
Abstract Interpretation (Proceedings of 4th International Conference,
VMCAI 2003, New York, NY, USA, January
9-11, 2003), volume 2575 of Lecture Notes in Computer Science,
pages 283-297, Springer-Verlag, 2003. .ps
Toh Ne Win, Michael Ernst, Stephen Garland, Dilsun Kirli, and Nancy Lynch.
Using simulated execution in verifying distributed algorithms.
International Journal on Software Tools for Technology Transfer
(STTT), 4:(1-10), 2003.
Edward Solovey. Simulation of Composite I/O Automata.
Masters of Engineering Thesis, MIT Department of Electrical
Engineering and Computer Science, Cambridge, MA, August 2003. .ps
2002
P. C. Attie. Wait-free Byzantine Consensus.
Information Processing Letters, vol. 83, no. 4, pp. 221-227,
August 2002. .ps
Paul Attie, Nancy Lynch, and Sergio Rajsbaum.
Boosting Fault-Tolerance in Asynchronous Message Passing Systems is
Impossible. Technical Report MIT-LCS-TR-877, MIT Laboratory for Computer
Science, Cambridge, MA, December 2002. .ps
Mohsen Bahramgiri, Mohammad Taghi Hajiaghayi, and Vahab S. Mirrokni.
Fault-tolerant and 3-Dimensional distributed topology control
algorithms in wireless multi-hop networks. Proceedings of the
11th IEEE International Conference on Computer Communications and
Networks (IC3N), pages 392-398, October 14-16, 2002, Miami,
Floria. .ps
Also, MIT Technical Report MIT-LCS-TR-862, Cambridge, MA 02139, 2002.
Omar Bakr and Idit Keidar. Evaluating the Running Time of a
Communication Round over the Internet. Proceedings of the 21st ACM Symposium on Principles of Distributed Computing (PODC '02),
Monterey, CA, USA, pages 243-252, July 2002. .ps
Ziv Bar-Joseph and Idit Keidar and Nancy Lynch.
Early-Delivery Dynamic Atomic Broadcast. In D. Malkhi,
editor, Distributed Computing (Proceedings of the
16th International Symposium on DIStributed Computing (DISC) October 2002,
Toulouse, France), volume 2508 of Lecture Notes in Computer
Science, pages 1-16, 2002. Springer-Verlag. .ps
Ziv Bar-Joseph, Idit Keidar, and Nancy Lynch. Early-Delivery
Dynamic Atomic Broadcast. Technical Report MIT-LCS-TR-840, MIT
Laboratory for Computer Science, Cambridge, MA, April 2002. .ps
Andrej Bogdanov, Stephen Garland, and Nancy A. Lynch.
Mechanical Translation of I/O Automaton Specifications into
First-Order Logic. In Doron Peled, Moshe Y. Vardi, editors,
Formal Techniques for Networked and Distributed Systems - FORTE 2002
(Proceedings of the 22nd IFIP WG 6.1 International Conference,
Houston, Texas, USA,
November 11-14, 2002), volume 2529 of Lecture
Notes in Computer Science, pages 364-368, Springer 2002. .pdf
Roberto De Prisco, Alan Fekete, Nancy Lynch, and Alex Shvartsman. A
Dynamic Primary Configuration Group Communication Service.
Technical Memo MIT-LCS-TR-873, MIT Laboratory for Computer Science,
Cambridge, MA, November 2002. Abstract/Paper.
Matthias Fitzi, Daniel Gottesman, Martin Hirt, Thomas Holenstein, and
Adam Smith. Detectable Byzantine Agreement Secure Against Faulty
Majorities. In Proceedings of the Twenty-First ACM Symposium on
Principles of Distributed Computing (PODC 2002), Monterey, CA, July,
2002. .pdf
Seth Gilbert and Nancy Lynch. Brewer's conjecture and the
feasibility of consistent, available, partition-tolerant web
services. Sigact News, 33(2), June 2002. .ps
Dilsun Kirli Kaynar, Anna Chefter, Laura Dean, Stephen J. Garland,
Nancy A. Lynch, Toh Ne Win, and Antonio Ramirez-Robredo.
Simulating Nondeterministic Systems at Multiple Levels of
Abstraction. In Tools Day held in conjunction with CONCUR'02, Brno, Czech
Republic, August 2002. .ps
Dilsun Kirli Kaynar, Anna Chefter, Laura Dean, Stephen Garland,
Nancy Lynch, Toh Ne Win, and Antonio Ramirez-Robredo. The IOA Simulator. Technical Report
MIT-LCS-TR-843, MIT Laboratory for Computer Science, Cambridge, MA,
July 2002. ps
Idit Keidar. Challenges in Evaluating Distributed Algorithms.
FuDiCo 2002: Proceedings of the International Workshop on Future Directions in
Distributed Computing (FuDiCo 2002), June 2002, Bertinoro, Italy. ps
I. Keidar and K. Marzullo. The Need for Realistic Failure Models in
Protocol Design. Position paper in the 4th International Survivability Workshop (ISW)
2001/2002, March 2002. .ps
Idit Keidar, Roger Khazan, Nancy Lynch and Alex Shvartsman.
An Inheritance-Based Technique for Building Simulation Proofs
Incrementally.
ACM Transactions on Software Engineering and
Methodology (TOSEM), 11(1):1-29, January 2002. Conference
version in ICSE, 2000, pages 478-487. .pdf
Idit Keidar and Roger Khazan.
A virtually synchronous group multicast algorithm for WANs: Formal
approach. SIAM Journal on Computing, Vol. 32, No. 1,
pp. 78-130, 2002. .ps
Roger Khazan. Formal Design and Analysis of a New Virtually
Synchronous Group Communication Service for Wide Area Networks.
Ph.D
Thesis, Department of Electrical Engineering and Computer Science,
Massachusetts Institute of Technology, Cambridge, MA, May 2002.
Carolos Livadas and Nancy A. Lynch. A Formal Venture into Reliable
Multicast Territory. In Doron Peled, Moshe Y. Vardi, editors,
Formal Techniques for Networked and Distributed Systems - FORTE 2002
(Proceedings of the 22nd IFIP WG 6.1 International Conference,
Houston, Texas, USA, November 11-14, 2002), volume 2529 of Lecture
Notes in Computer Science, pages 146-161, Springer 2002. .pdf
Also, full version as Technical Report MIT-LCS-TR-868, MIT
Laboratory for Computer Science, Cambridge, MA, November 2002.
Carolos Livadas and Nancy A. Lynch. A Formal Venture into Reliable
Multicast Territory. Technical Report MIT-LCS-TR-868, MIT
Laboratory for Computer Science, Cambridge, MA, November 2002. .pdf
Carolos Livadas and Idit Keidar. The Case for Exploiting Packet Loss
Locality in Multicast Loss Recovery. Technical Report MIT/LCS/TR-867,
MIT Laboratory for Computer Science, Cambridge, MA, Oct. 2002. .pdf
Nancy Lynch, Dahlia Malkhi, David Ratajczak. Atomic Data Access in
Content Addressable Networks. In
P. Druschel, F. Kaashoek, and A. Rowstron, editors, Peer-to-Peer
Systems (First International Workshop on
Peer-to-Peer Computing, Cambridge, MA, March 2002), volume 2429 of
Lecture Notes in Computer Science, pages 295-305, Springer, 2002.
.pdf
Nancy Lynch and Alex Shvartsman. Communication and Data Sharing
for Dynamic Distributed Systems. In A. Schiper,
A.A. Shvartsman, H. Weatherspoon, B.Y. Zhao, editors, Future
Directions in Distributed Computing: Research and Position Papers (FuDiCo 2002: Proceedings of
the International Workshop on Future Directions in Distributed
Computing, Bertinoro,Italy, June 2002), volume 2584 of Lecture Notes
in Computer Science, pages 62-67, Springer-Verlag, 2003.
.pdf
Nancy Lynch and Alex Shvartsman. RAMBO: A Reconfigurable
Atomic Memory Service for Dynamic Networks. In D. Malkhi,
editor, Distributed Computing (Proceedings of the
16th International Symposium on DIStributed Computing (DISC) October 2002,
Toulouse, France), volume 2508 of Lecture Notes in Computer
Science, pages 173-190, 2002. Springer-Verlag. .pdf Also,
Technical Report MIT
Laboratory for Computer Science, Technical Report MIT-LCS-TR-856,
Cambridge, MA, 2002.
Nancy Lynch and Alex Shvartsman. RAMBO: A Reconfigurable Atomic
Memory Service for Dynamic Networks. Technical Report MIT-LCS-TR-856,
MIT Laboratory for Computer Science, Cambridge, MA, 2002. .ps
Michael J. Tsai. Code Generation for the IOA Language. Master of Engineering Thesis, Massachusetts Institute of
Technology, Cambridge, MA, June 2002. Abstract
and .pdf
Yoshinobu Kawabe and Ken Mano. Verifying the Nepi network programming
system with IOA-Toolkit. Proceedings of the 9th Workshop on
Foundations of Software Engineering (FOSE '02), 2002. In Japanese.
2001
P.C. Attie and E.A. Emerson. Synthesis of concurrent systems for
an atomic read/write model of computation.
ACM Transactions on Programming Languages and Systems,
vol. 23, no. 2, pp. 187-242, March 2001. .pdf
Extended abstract appears in ACM Symposium on the Principles of Distributed Computing
(PODC) 1996.
Paul C. Attie and Nancy A. Lynch. Dynamic Input/Output Automata: a
Formal Model for Dynamic Systems.
In K. G. Larsen and M. Nielsen, editors, CONCUR 2001 - Concurrency
Theory: 12th International Conference on Concurrency Theory,
Aaalborg, Denmark, August 20-25, 2001, Proceedings, volume 2154 of
Lecture Notes in Computer Science, pages 137-151, 2001.
Springer-Verlag. Postscript
Andrej Bogdanov. Formal verification of simulations between
I/O automata. Master of Engineering thesis, Department of Electrical Engineering
and Computer Science, Massachusetts Institute of Technology,
Cambridge, MA, September 2001. pdf.
Elizabeth Borowsky, Eli Gafni, Nancy Lynch, and Sergio Rajsbaum.
The BG Distributed Simulation Algorithm.
Distributed Computing, 14:127-146, 2001. ps.
Bogdan S. Chlebus, Roberto De Prisco, and Alex A. Shvartsman.
Performing tasks on synchronous restartable message-passing
processors. Distributed Computing, 14:49-64, 2001. Postscript
Gregory V. Chockler, Idit Keidar, and Roman Vitenberg. Group
Communication Specifications: A Comprehensive Study. ACM
Computing Surveys, 33(4):1-43, December 2001. .pdf
Laura G. Dean. Improved Simulation of Input/Output Automata. Master of Engineering Thesis,
Massachusetts Institute of Technology, Cambridge, MA, September 2001.
Alan Fekete and Idit Keidar:
A Framework for Highly Available Services Based on Group
Communication. IEEE International Workshop on Applied
Reliable Group Communication (WARGC), pages 57-62, held in conjunction with ICDCS 2001, April 2001. Postscript
Alan Fekete, Nancy Lynch, and Alex Shvartsman. Specifying and Using a Partitionable Group Communication
Service. ACM
Transactions on Computer Systems, 19(2):171-216, May 2001.
Stephen J. Garland and Nancy A. Lynch and Mandana Vaziri. IOA: A
Language for Specifying, Programming and Validating Distributed Systems.
User and Reference Manual. Laboratory for Computer Science, Massachusetts
Institute of Technology, Cambridge, MA 02139, October 2001. Postscript.
Kyle Ingols and Idit Keidar:
Availability Study of Dynamic Voting Algorithms.
21st IEEE International Conference on Distributed Computing
Systems (ICDCS), pages 247-254, April 2001.
Previous version: MIT Technical Memorandum MIT-LCS-TM-611,
November 2000. Postscript
Idit Keidar and Sergio Rajsbaum.
On the Cost of Fault-Tolerant Consensus When There Are No Faults -
A Tutorial.
MIT Technical Report MIT-LCS-TR-821, May 24 2001.
Preliminary version in SIGACT News 32(2), Distributed Computing
column, pages 45-63, June 2001 (published in May 15th).
Abstract/Paper.
Carolos
Livadas, Idit
Keidar, and Nancy A. Lynch. Designing a Caching-Based Reliable
Multicast Protocol. Proceedings of the International Conference on
Dependable Systems and Networks (DSN'01), Fast Abstracts Supplement,
pages B44-B45, Gothenburg, Sweden, July 2001. [Abstract/Postscript]
Victor Luchangco. Memory Consistency Models for High Performance
Distributed Computing. Ph.D Thesis, Massachusetts Institute of
Technology, Cambridge, Massachusetts, September 2001.
Nancy Lynch, Roberto Segala, and Frits Vaandrager. Hybrid I/O
Automata Revisited. In Maria Domenica Di Benedetto and Alberto
Sangiovanni-Vincentelli, editors Hybrid Systems: Computation and
Control. Fourth International Workshop (HSCC'01, Rome, Italy, March
2001, volume 2034 of Lecture Notes in Computer Science,
pages 403-417, 2001. Springer-Verlag. Postscript.
Long version is Technical Report MIT/LCS/TR-827, MIT Laboratory for
Computer Science, July 2001.
Michael J. Tsai. Abstract Data Types (ADTs) for IOA Code Generation.
Manuscript, September 2001.
2000
Tadashi Araragi, Paul Attie, Idit Keidar, Kiyoshi Kogure,
Victor Luchangco, Nancy Lynch, and Ken Mano.
On Formal Modeling of Agent Computations.
In J.L. Rash, C.A. Rouff, W. Truszkowski, D. Gordon,
M.G. Hinchey, editors, Formal Approaches to Agent-Based Systems
(First International Workshop on Formal Approaches to Agent-Based
System (FAABS 2000), Greenbelt, Maryland, April, 2000), volume 1871
of Lecture Notes in Artificial Intelligence, pages 48-62,
Springer-Verlag, 2000.
pdf,
abstract.
Ziv Bar-Joseph, Idit Keidar, Tal Anker, and Nancy Lynch:
QoS Preserving Totally Ordered Multicast.
5th International Conference On Principles
Of Distributed Systems (OPODIS), pages 143-162, Paris, France,
December, 2000. Postscript
Ziv Bar-Joseph, Idit Keidar, Tal Anker, and Nancy Lynch. QoS
Preserving Totally Ordered Multicast. MIT Technical Report
MIT-LCS-TR-796, January 2000. Postscript
Soma Chaudhuri, Maurice Herlihy, Nancy A. Lynch, and Mark
R. Tuttle. Tight Bounds for k-Set Agreement.
Journal of the ACM, pages 47(5):912-943, September, 2000. .pdf
Roberto DePrisco, Butler Lampson, and Nancy Lynch. Fundamental
Study: Revisiting the PAXOS algorithm. Theoretical Computer
Science, 243:35-91, 2000. Elsevier Science B.V. PDF
Buckhard Englert and Alexander A. Shvartsman. Graceful Quorum
Reconfiguration in a Robust Emulation of Shared Memory.
International Conference on Distributed Computer Systems (ICDCS'2000),
pages 454-463, 2000. PDF
Stephen J. Garland and Nancy A. Lynch. Using
I/O Automata for Developing Distributed Systems. In Gary T. Leavens and Murali Sitaraman, editors,
Foundations of Component-Based Systems, pages 285-312, Cambridge
University Press, 2000. Abstract/Postscript
Chryssis Georgiou and Alex A. Shvartsman. Cooperative Computing
with Fragmentable and Mergeable Groups. Technical Report
MIT/LCS/TR-802, Laboratory for Computer
Science, Massachusetts Institute of Technology, 2000. Postscript
Kyle W. Ingols. Availability Study of Dynamic Voting Algorithms.
M.Eng. thesis, MIT Department of Electrical Engineering and Computer
Science, Cambridge, MA, May 5, 2000. Postscript
Idit Keidar and Danny Dolev. Totally Ordered Broadcast in the Face of
Network Partitions. Exploiting Group Communication for Replication in
Partitionable Networks. Chapter 3 of Dependable Network Computing,
D. Avresky Editor, pages 51-75, Kluwer Academic Publications, January 2000. Postscript
Idit Keidar and Roger Khazan. A Client-Server Approach to Virtually
Synchronous Group Multicast: Specifications and Algorithms.
IEEE 20th International Conference on
Distributed Computing Systems (ICDCS), pages 344-355, Taipei,
Taiwan, April 2000.
Abstract
(technical report version).
Idit Keidar, Roger Khazan, Nancy Lynch and Alex Shvartsman.
An Inheritance-Based Technique for Building Simulation Proofs
Incrementally.
ACM Transactions on Software Engineering and
Methodology (TOSEM), 11(1):1-29, January 2002. Conference
version in ICSE, 2000, pages 478-487. Postscript
I. Keidar, J. Sussman, K. Marzullo, and D. Dolev. A
Client-Server Oriented Algorithm for Virtually Synchronous Group Membership in WANs.
IEEE 20th International Conference on
Distributed Computing Systems (ICDCS), pages 356-365, Taipei,
Taiwan, April 2000.
Abstract
(technical report version).
Carolos Livadas, John Lygeros, and Nancy A. Lynch. High-Level
Modeling and Analysis of TCAS. Proceedings of IEEE, Special Issue on
Hybrid Systems: Theory & Applications, 88(7):926-948, July 2000. Abstract
John Lygeros and Nancy Lynch. Conditions for Safe Deceleration of
Strings of Vehicles. California PATH Research Report
UCB-ITS-PRR-2000-2, California PATH Program, Institute of
Transportation Studies, University of California, Berkeley, January 2000.
Gregory Malewicz, Alexander Russell, and Alex Shvartsman.
Distributed Cooperation in the Absence of Communication.
Technical Report MIT-LCS-TR-804, Laboratory for Computer Science,
Massachusetts Institute of Technology, Cambridge, MA. Postscript
Anna Pogosyants, Roberto Segala, and Nancy Lynch.
Verification of the randomized consensus algorithm of Aspnes and
Herlihy: a case study. Distributed Computing,
13(3):155-186, 2000. .pdf
J. Antonio Ramirez-Robredo. Paired Simulation of I/O Automata.
Masters thesis. Department of Electrical Engineering and Computer
Science, Massachusetts Institute of Technology, Cambridge, MA, September,
2000.
Igor Tarashchanskiy. Virtual Synchrony Semantics: Client-Server
Implementation. Masters thesis. MIT Department of Electrical
Engineering and Computer Science, Cambridge, MA, September, 2000. Postscript
1999
Tal Anker, Danny Dolev and Idit Keidar. Fault Tolerant Video-on-Demand
Services. In the 19th International Conference on Distributed Computing
Systems (ICDCS), pages 244-252. June 1999. Postscript
Oleg Cheiner and Alex Shvartsman. Implementing an eventually-serializable
data service as a distributed system building block. In M. Mavronicolas,
M. Merritt, and N. Shavit, editors, Networks in Distributed Computing,
volume 45 of DIMACS Series in Discrete Mathematics and Theoretical Computer
Science, pages 43--72. American Mathematical Society, 1999.
.ps
Roberto DePrisco. On Building Blocks for Distributed Systems.
Ph.D thesis, Department of Electrical Engineering and Computer Science,
Massachusetts Institute of Technology, Cambridge, MA 02139, December
1999. .ps
Roberto De Prisco, Alan Fekete, Nancy Lynch, and Alex Shvartsman. A
Dynamic Primary Configuration Group Communication Service. In Prasad
Jayanti, editor, Distributed Computing (Proceedings of DISC'99 - 13th International
Symposium on Distributed Computing, Bratislava, Slovak Republic, September
1999), volume 1693 of Lecture Notes in Computer Science, pages 64-78, 1999. Springer-Verlag-Heidelberg. Abstract/Paper.
Shlomi Dolev and Roberto Segala and Alex Shvartsman. Dynamic Load
Balancing with Group Communication 6th International Colloquium
on Structural Information and Communication Complexity
(SIROCCO'99). .ps.
Alan Fekete, Nancy Lynch, and Alex Shvartsman. Specifying and Using a Partitionable Group Communication
Service. MIT Laboratory for Computer Science, Cambridge, MA Technical
Memo MIT/LCS/TM-570b, June 1999.
Alan Fekete, David Gupta, Victor Luchangco, Nancy Lynch, and Alex
Shvartsman. Eventually-Serializable Data Services. Theoretical
Computer Science, 220(1):113--156, June 1999. Special Issue on Distributed
Algorithms. ps
Jason Hickey, Nancy Lynch,
Robbert van Renesse. Specifications and Proofs for Ensemble Layers.
Fifth International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS '99), Amsterdam, the Netherlands, March
1999. Springer-Verlag. Postscript
Henrik Ejersbo Jensen. Abstraction-Based Verification of Distributed
Systems. Ph.D thesis, Department of Computer Science, Institute
for Electronic Systems, Aalborg University, Aalborg, Denmark, June 1999.
R-99-5005. .ps
Idit Keidar, Jeremy Sussman, Keith Marzullo and Danny Dolev.
A Client-Server Oriented Algorithm for Virtually
Synchronous Group Membership in WANs.
MIT Technical Memorandum MIT-LCS-TM-593, June 1999.
Also: University of California, San Diego, Technical Report CS99-623.
ps,
ps.gz,
pdf,
abstract
Idit Keidar and Roger Khazan. A Client-Server Approach to
Virtually Synchronous Group Multicast: Specifications, Algorithms,
and Proofs. MIT Technical Report MIT-LCS-TR-794, November 1999.
ps,
ps.gz,
pdf,
abstract.
Carolos Livadas,
John Lygeros, and Nancy A. Lynch.
High-Level Modeling and Analysis of TCAS. Proceedings
of the 20th IEEE Real-Time Systems Symposium, pages 115-125, Phoenix, Arizona, December,
1999. Abstract
Nancy Lynch I/O Automaton
Models and Proofs for Shared-Key Communication Systems Technical
Report MIT/LCS/TR-789, Laboratory for Computer Science, Massachusetts Institute
of Technology, Cambridge, MA, August, 1999.
Nancy Lynch I/O Automaton
Models and Proofs for Shared-Key Communication Systems Proceedings of
the 12th IEEE Computer Security Foundations Workshop (CSFW'99), Mordana,
Italy, June 28-30, 1999. (Abstract/Paper).
Nancy Lynch, Nir Shavit, Alex Shvartsman, and Dan Touitou. Timing
conditions for linearizability in uniform counting networks. Theoretical
Computer Science, 220(1):67--91, June 1999. Special Issue on Distributed
Algorithms. .pdf.
Jeremy Sussman, Idit Keidar and Keith Marzullo. Optimistic Virtual
Synchrony. MIT Technical Report MIT-LCS-TR-792, November 1999.
Postscript
Roman Vitenberg, Idit Keidar, Gregory V. Chockler and Danny Dolev. Group
Communication Specifications: A Comprehensive Study. MIT Technical
Report MIT-LCS-TR-790, September 1999. Postscript
Daniel Yates, Nancy Lynch, Victor Luchangco, and Margo Seltzer. I/O
Automaton Model of Operating System Primitives Bachelors Thesis, Harvard
University, May 1999. Thesis
(compressed .ps)
1998
Soma Chaudhuri, Maurice
Herlihy, Nancy A. Lynch,
and Mark R. Tuttle. Tight bounds for k-set agreement Technical
Report 98/4, Digital Equipment Corporation, Cambridge Research Lab, Cambridge,
MA 02139, May, 1998.Compressed
Postscript
Anna E. Chefter.
A Simulator for the IOA Language Master of Engineering and Bachelor
of Science in Computer Science and Engineering Thesis,
Massachusetts Institute of Technology, Cambridge, MA, May 1998.
Oleg Cheiner and Alex A. Shvartsman. Implementation of an eventually
serializable data service. In Proceedings of the 17th Annual ACM
Symposium on the Principles of Distributed Computing, Puerta Vallarta,
Mexico, June 1998. (Short paper). .ps
Roberto De Prisco, Alan
Fekete, Nancy Lynch,
and Alex Shvartsman. A
Dynamic View-Oriented Group Communication Service. In Proceedings
of the 17th Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed
Computing (PODC'98), Puerto Vallarta, June-July, 1998. Abstract/Paper
Ekaterina Dolginova. Safety verification of automated car maneuvers.
Master of Engineering, Department of Electrical Engineering and Computer Science,
Massachusetts Institute of Technology, Cambridge, MA 02139, May
1998. Postscript.
Shlomi Dolev, Roberto Segala, and Alex Shvartsman. Dynamic load balancing
with group communication. Technical Memo MIT/LCS/TM-588, Laboratory
for Computer Science, Massachusetts Institute of Technology, Cambridge,
MA, 1998. .ps
Alan Fekete, Frans Kaashoek and Nancy
Lynch. Implementing Sequentially-Consistent Shared Objects Using
Group and Point-to-Point Communication . Journal
of the ACM, 45(1):35-69, January, 1998.
Matteo Frigo and Victor Luchangco. Computation-centric memory models.
In ACM Symposium on Parallel Algorithms and Architectures (SPAA'98),
pages 240--249, Puerto Vallarta, Mexico, June-July 1998. .ps
Stephen J. Garland
and Nancy A. Lynch. The
IOA Language and Toolset: Support for Designing, Analyzing, and Building
Distributed Systems. Technical
Report MIT/LCS/TR-762, Laboratory for Computer Science, Massachusetts
Institute of Technology, Cambridge, MA, August 1998 (original version:
September 25, 1997).
Stephen J. Garland and Nancy A. Lynch. The IOA language and toolset:
Support for mathematics-based distributed programming, 1998. Manuscript.
Henrik Jensen and Nancy Lynch. A proof of Burns N-Process mutual
exclusion algorithm using abstraction. In Bernhard Steffen, editor,
Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98,
Lisbon, Portugal, April 1998), volume 1384 of Lecture Notes in Computer
Science, pages 409--423. Springer, 1998. Postscript
Roger Khazan. Group Communication as a Base for a Load-Balancing
Replicated Data Service. Masters thesis, Department of Electrical
Engineering and Computer Science, Massachusetts Institute of Technology,
Cambridge, MA 02139, May 1998. (Compressed
Postscript
1.35M)
Roger Khazan, Alan Fekete, and Nancy Lynch. Multicast Group Communication
as a Base for a Load-Balancing Replicated Data Service. 12th International
Symposium on Distributed Computing (DISC98), September 1998. (Compressed
Postscript
500K)
Carolos Livadas and
Nancy A. Lynch. Formal
Verification of Safety-Critical Hybrid Systems. In S. Sastry and
T.A. Henzinger, editors, Hybrid Systems: Computation and Control (First
International Workshop, HSCC'98, Berkeley, CA, USA, April, 1998), number
1386 in Lecture Notes in Computer Science, pages 253--272. Springer Verlag,
1998. (Abstract/Postscript)
John Lygeros and Nancy Lynch. Strings of vehicles: Modeling and safety
conditions. In S. Sastry and T.A. Henzinger, editors, Hybrid Systems:
Computation and Control (First International Workshop, HSCC'98, Berkeley,
CA, USA, April, 1998), number 1386 in Lecture Notes in Computer Science,
pages 273--288. Springer Verlag, 1998. Postscript
Dahlia Malkhi, Mike Reiter, and Nancy Lynch. A correctness condition
for memory shared by Byzantine processes, 1998. Manuscript.
Roberto Segala, Rainer Gawlick, Jorgen Sogaard-Andersen, and Nancy Lynch.
Liveness in timed and untimed systems. Information and Computation,
141(2):119--171, March 1998. Postscript
Roberto Segala. Hybrid I/O automata for the compositional analysis
of hybrid systems. In Book of Abstracts of the conference of Mathematical
Theory for Networks and Systems (MTNS), Padova, Italy, July 1998. An extended
version was submitted for publication in the conference proceedings.
Nir Shavit and Asaph Zemach. Combining funnels: A new twist on an
old tale. In Proceedings of the 17th Annual ACM SIGACT-SIGOPS Symposium
on Principles of Distributed Computing, pages 61--70, Puerto Vallarta,
Mexico, June-July 1998. .pdf
N. Shavit, E. Upfal, and A. Zemach. A steady state analysis of diffracting
trees. Theory of Computing Systems (formerly Mathematical Systems
Theory), 31(4):403--423, July/August 1998. Special issue: ACM Symposium
on Parallel Algorithms and Architectures. .ps
Mark Smith. Reliable message delivery and conditionally-fast transactions
are not possible without accurate clocks. In Proceedings of the
17th Annual ACM Symposium on the Principles of Distributed Computing, pages
163--171, Puerto Vallarta, Mexico, June 1998. .pdf
Mandana Vaziri and Gerard Holzmann. Automatic generation of invariants
in spin. In 4th International Workshop on SPIN, pages 129--139,
Paris, France, November 1998. ps
Mandana Vaziri. Translating IOA to Promela, September 1998. Manuscript.
Mandana Vaziri, Nancy Lynch, and Jeannette Wing. Proving correctness of a controller
algorithm for the RAID level 5 system. Digest of papers from
the Twenty-Eighth Annual International Symposium on Fault-Tolerant
Computing, pages 16-25, Munich, Germany, June 1998. pdf
1997
Y. Afek, B. Awerbuch, E. Gafni, Y. Mansour, A. Rosen, and N. Shavit.
Slide: the key to polynomial end-to-end communication. Journal
of Algorithms, 22:158--186, 1997.
Elizabeth Borowsky, Eli Gafni, Nancy
Lynch and Sergio Rajsbaum. The BG Distributed Simulation Algorithm.
Technical Memo MIT/LCS/TM-573, Laboratory for Computer Science, Massachusetts
Institute of Technology, Cambridge, MA 02139, December, 1997. Also, submitted
for journal publication. (Abstract/Postscript)
Michael S. Branicky,
Ekaterina Dolginova,
and Nancy Lynch. A Toolbox
for Proving and Maintaining Hybrid Specifications. In Panos
J. Antsaklis et al,
editor, Hybrid Systems IV (HS'96, Cornell University, Ithaca, NY, October
12-16, 1996), volume 1273 of Lecture Notes in Computer Science, pages
18-30. Springer-Verlag 1997. (Abstract/Postscript)
Oleg Cheiner. Implementation
and Evaluation of an Eventually-Serializable Data Service. Master
of Engineering Thesis, Department of Electrical Engineering and Computer
Science, Massachusetts Institute of Technology, September 1997.
Bogdan Chlebus, Roberto
De Prisco, and Alex Shvartsman.
Performing Tasks on Restartable Message-Passing Processors. In
Marios Mavronicolas and Philippas Tsigas, editors, Proceedings of 11th
International Workshop on Distributed Algorithms (WDAG'97, Saarbrucken,
Germany, September 1997), volume 1320 of Lecture Notes in Computer Science,
pages 96-110. Springer-Verlag 1997. (Abstract/Postscript)
Darren Cofer, John Maloney, Rosa Weber, George Pappas, Shankar Sastry,
John Lygeros, and Nancy Lynch. Formal specification and analysis of the
center-TRACON automation systems (CTAS). Final Report SST-C97-002, Honeywell
Technology Center, September 30 1997. Prepared for Langley Research Center
and NEXTOR: FAA Center of Excellence in Aviation Operations Research.
Giovanni Della Libera and Nir Shavit. Reactive diffracting trees. In
Proceedings of the 9th Annual ACM Symposium on Parallel Algorithms and
Architectures (SPAA), Newport, Rhode Island, June 1997.
Roberto De Prisco,Butler
Lampson, and Nancy Lynch.
Revisiting the Paxos algorithm. In Marios Mavronicolas and Philippas
Tsigas, editors, Proceedings of 11th International Workshop on Distributed
Algorithms (WDAG'97, Saarbrucken, Germany, September 1997), volume 1320
of Lecture Notes in Computer Science, pages 111-125. Springer-Verlag 1997.
(Abstract/Postscript)
Roberto De Prisco. Revisiting
the Paxos algorithm. Master of Science Thesis, Department of Electrical
Engineering and Computer Science, Massachusetts Institute of Technology,
June 1997. Also, Technical Report MIT/LCS/TR-717, Laboratory for Computer
Science, Massachusetts Institute of Technology. (Abstract/Postscript)
Danny Dolev and Nir Shavit. Bounded concurrent time stamping. SIAM
Journal on Computing, 26(2):418--455, April 1997.
Ekaterina Dolginova
and Nancy Lynch. Safety
Verification for Automated Platoon Maneuvers: A Case Study. In International
Workshop on Hybrid and Real-Time Systems (HART'97, Grenoble, France, March
26-28, 1997), volume 1201 of Lecture Notes in Computer Science, pages 154-170.
Springer-Verlag 1997. (Abstract/Postscript)
Alan Fekete,
Nancy Lynch, and Alex
Shvartsman. Specifying and Using a Partitionable Group Communication
Service. Proceedings of the Sixteenth Annual ACM Symposium on Principles
of Distributed Computing (PODC'97, Santa Barbara, CA), pages 53-62, August
1997. (Abstract/Postscript)
Also, Technical Memo MIT/LCS/TM-570, Laboratory for Computer Science,
Massachusetts Institute of Technology, October 1997. (Compressed
Postscript)
Stephen J. Garland and Nancy A. Lynch and Mandana Vaziri. IOA: A
Language for Specifying, Programming and Validating Distributed Systems.
User and Reference Manual. Laboratory for Computer Science, Massachusetts
Institute of Technology, Cambridge, MA 02139, January 2001. Postscript.
Datta N. Godbole and John Lygeros. Safety and throughput evaluation
of automated highway systems. In 1997 American Control Conference, June
1997.
Gunnar Hoest and Nir
Shavit Towards a Topological Characterization of Asynchronous Complexity
Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed
Computing, pages 199-208, Santa Barbara, CA, August 1997.
(Abstract/Postscript)
Gunnar Hoest. Towards a topological characterization of complexity in
asynchronous, distributed systems. Master's thesis, Department of Electrical
Engineering and Computer Science, Massachusetts Institute of Technology,
Cambridge, MA 02139, September 1997. .ps
Paris Christos Kanellakis, Alex
Allister Shvartsman. Fault-Tolerant Parallel Computation. Kluwer
Academic Publishers, Boston, MA, 1997. (Abstract/Information)
Carolos Livadas, Formal
Verification of Safety-Critical Hybrid Systems, Master of Engineering
Thesis, Department of Electrical Engineering and Computer Science, Massachusetts
Institute of Technology, September 1997. (Abstract/Postscript)
Also, Technical Report MIT/LCS/TR-730, Laboratory for Computer Science,
Massachusetts Institute of Technology, September 1997.
Victor Luchangco.
Precedence-Based Memory Models. In Marios Mavronicolas and Philippas
Tsigas, editors, Proceedings of 11th International Workshop on Distributed
Algorithms (WDAG'97, Saarbrucken, Germany, September 1997), volume 1320
of Lecture Notes in Computer Science. Springer-Verlag 1997. (Abstract/Postscript)
John Lygeros, Claire Tomlin, and Shankar Sastry. Multi objective
hybrid controller synthesis. In International Workshop on Hybrid
and Real-Time Systems (HART'97), Grenoble, France, March 1997.
John Lygeros, Claire Tomlin, and Shankar Sastry. Multi-objective
hybrid controller synthesis. In 36th IEEE Conference on Decision
and Control, San Diego, California, December 1997.
John Lygeros
and Nancy Lynch. On the
Formal Verification of the TCAS Conflict Resolution Algorithms. Proceedings
of the 36th IEEE Conference on Decision and Control, San Diego, CA, December
1997. (Summary/Postscript)
Nancy Lynch, and Alex
Shvartsman. Robust emulation of shared memory using dynamic quorum-acknowledged
broadcasts. Twenty-Seventh Annual International Symposium on Fault-Tolerant
Computing (FTCS'97), pages 272-281, Seattle, Washington, USA, June 1997.
IEEE (Abstract/Postscript)
George Pappas, Shankar Sastry, John Lygeros, and Nancy Lynch. Modeling,
specification, and safety analysis of CTAS. Final report, University
of California, September 30 1997. Prepared for Langley Research Center
and NEXTOR: FAA Center of Excellence in Aviation Operations Research.
George Pappas, Claire Tomlin, John Lygeros, Datta Godbole, and Shankar
Sastry. A next generation architecture for air traffic management systems.
In 36th IEEE Conference on Decision and Control, San Diego, CA, December
1997. Extended abstract.
Anna Pogosyants,
Roberto Segala, and Nancy
Lynch.Verification of the Randomized Consensus Algorithm of Aspnes
and Herlihy: a Case Study. In Marios Mavronicolas and Philippas
Tsigas, editors, Proceedings of 11th International Workshop on Distributed
Algorithms (WDAG'97, Saarbrucken, Germany, September 1997), volume 1320
of Lecture Notes in Computer Science, pages 111-125. Springer-Verlag 1997.
Also, Technical Memo MIT/LCS/TM-555, Laboratory for Computer Science, Massachusetts
Institute of Technology. (Abstract/Postscript)
Roberto Segala. Compositional verification of randomized distributed
algorithms. In COMPOS, 1997. Invited talk.
Roberto Segala. Quiescence, fairness, testing and the notion of implementation.
Information and Computation, 130(2):194--210, November 1997.
Nir Shavit, and Dan
Touitou. Elimination Trees and the Construction of Pools and Stacks.Theory
of Computing Systems (formerly Mathematical Systems Theory), volume 30,
pages 645-670, 1997. (Postscript)
N. Shavit and D. Touitou. Software transactional memory. Distributed
Computing, 10(2):99--116, February 1997.
Mark Smith. Formal Verification of TCP and T/TCP. Ph.D thesis, Department
of Electrical Engineering and Computer Science, Massachusetts Institute
of Technology, Cambridge, MA 02139, September 1997. .ps
Mandana Vaziri and Nancy Lynch. Proving correctness of a controller
algorithm for the RAID level 5 system. Technical Memo MIT/LCS/TM-576,
Laboratory for Computer Science, Massachusetts Institute of Technology,
545 Technology Square, Cambridge, MA 02139, December 1997. .ps
1996
S. Abiteboul, G. M. Kuper, H. G. Mairson, A. A. Shvartsman, and M. Y.
Vardi. In memoriam: Paris C. Kanellakis, a technical obituary. ACM Computing
Surveys, March 1996.
Hagit Attiya, Amir Herzberg, and Sergio Rajsbaum. Optimal clock synchronization
under different delay assumptions. SIAM Journal on Computing, April 1996.
Baruch Awerbuch, Boaz Patt-Shamir, and George Varghese. Self-stabilizing
end-to-end communication. Journal of High Speed Networks, 5(4):365--381,
1996.
Jonathan F. Buss, Paris C. Kanellakis, Prabhakar L. Ragde, and Alex
A. Shvartsman. Parallel Algorithms with Processor Failures and Delays.
Journal of Algorithms, Volume 10, pages 45-86, January 1996. (Abstract/Postscript)
Giovanni Della-Libera.
Dynamic Diffracting Trees. Master of Engineering Thesis, Department
of Electrical Engineering and Computer Science, Massachusetts Institute
of Technology, July 1996. (Abstract/Postscript)
Alan Fekete, David Gupta, Victor Luchangco, Nancy Lynch, and Alex Shvartsman.
Eventually-serializable data services. In Proceedings of the Fifteenth
Annual ACM Symposium on Principles of Distributed Computing, pages 300--309,
Philadelphia, PA, May 1996. .pdf
H. Galeana-Sanchez and S. Rajsbaum. Cycle pancyclism in tournaments
II. Graphs and Combinatorics, 12:9--16, 1996.
Rainer Gawlick, Charles Kalmanek, and K. G. Ramakrishnan. On-line routing
for permanent virtual circuits. Computer Communications, 19:235--244,
1996.
Constance Heitmeyer and Nancy Lynch. Formal verification of real-time
systems using timed automata. In Constance Heitmeyer and Dino Mandrioli,
editors, Formal Methods for Real-Time Computing, Trends in Software,
chapter 4, pages 83--106. John Wiley & Sons Ltd, April 1996.
Maurice Herlihy, Nir Shavit, and Orli Waarts. Linearizable counting
networks. Distributed Computing, (9):193--203, 1996.
Gunter Leeb and Nancy
Lynch. Proving Safety Properties of the Steam Boiler Controller.
In Jean-Raymond Abrial, Egon Boerger, and Hans Langmaack, editors, Proceedings
of Formal Methods for Industrial Applications: Specifying and Programming
the Steam Boiler Control, volume 11654 of Lecture Notes in Computer Science,
Springer-Verlag 1996. (Abstract/Postscript)
Nancy Lynch. Distributed
Algorithms. Morgan Kaufmann Publishers, San Mateo, CA, 1996. (Summary/Table
of Contents) To order, please contact Morgan
Kaufmann Publishers.
Nancy Lynch. A Three-Level
Analysis of a Simple Acceleration Maneuver, with Uncertainties. Proceedings
of the Third AMAST Workshop on Real-Time Systems, pages 1-22, Salt Lake
City, Utah, March 1996. (Abstract/Postscript)
Nancy Lynch. Modelling
and verification of automated transit systems, using timed automata, invariants
and simulations. In R. Alur, T. Henzinger, and E. Sontag, editors,
Hybrid Systems III: Verification and Control (DIMACS/SYCON Workshop on
Verification and Control of Hybrid Systems, New Brunswick, New Jersey,
October 1995), volume 1066 of Lecture Notes in Computer Science, pages
449-463. Springer-Verlag 1996. (Abstract/Postscript)
Nancy Lynch and Sergio
Rajsbaum. On the Borowsky-Gafni Simulation Algorithm. Proceedings
of ISTCS 1996: The Fourth Israel Symposium on Theory of Computing and Systems,
pages 4-15, Jerusalem, Israel, June 1996. Also, Proceedings of the Fifteenth
Annual ACM Symposium on Principles of Distributed Computing, page 57, Philadelphia,
PA, May 1996. (Abstract/Postscript).
Nancy Lynch, Nir
Shavit, Alex Shvartsman,
and Dan Touitou. Counting networks are practically linearizable.
In Proceedings of the Fifteenth Annual ACM Symposium on Principles of
Distributed Computing, pages 280-289, Philadelphia, PA, May 1996. (Abstract/Postscript)
Nancy Lynch, Roberto Segala, Frits Vaandrager, and
H. B. Weinberg. Hybrid I/O Automata. In R. Alur,
T. Henzinger, and E. Sontag, editors, Hybrid Systems III: Verification
and Control (DIMACS/SYCON Workshop on Verification and Control of
Hybrid Systems, New Brunswick, New Jersey, October 1995), volume 1066
of Lecture Notes in Computer Science, pages 496-510. Springer-Verlag
1996. (Abstract/Postscript)
Nancy Lynch and Frits
Vaandrager. Forward and backward simulations -- Part II: Timing-Based
systems. Information and Computation, 128(1):1-25, July
1996.(Abstract/Postscript).
Nancy Lynch and Frits
Vaandrager. Action Transducers and Timed Automata Formal
Aspects of Computing, 8(5):499-538, 1996. .ps
Tsvetomir P. Petrov, Anya Pogosyants, Victor Luchangco, Stephen J. Garland, and
Nancy A.
Lynch. Computer-Assisted Verification of an Algorithm for
Concurrent Timestamps. In Reinhard Gotzhein and Jan
Bredereke, editors, Formal Description Techniques IX: Theory,
Applications, and Tools (FORTE/PSTV'96: Joint International Conference
on Formal Description Techniques for Distributed Systems and
Communication Protocols, and Protocol Specification, Testing, and
Verification, Kaiserslautern, Germany, October 1996), pages
29--44. Chapman & Hall, 1996. (Abstract/Postscript)
Nir Shavit and Dan Touitou. Sofware transactional memory. Technical
Memo MIT/LCS/TM-675, Laboratory for Computer Science, Massachusetts Institute
of Technology, Cambridge, MA 02139, 1996.
Nir Shavit, and Asaph
Zemach. Diffracting Trees. ACM Transactions on Computer Systems,
14(4):385-428, November 1996. (Postscript)
Nir Shavit, Eli Upfal,
and Asaph Zemach. A Steady State Analysis of Diffracting Trees.
Proceedings of the 8th Annual ACM Symposium on Parallel Algorithms and
Architectures (SPAA'96, Padua, Italy), pages 33-41, June 1996. (Postscript)
Mark Smith. Formal verification of communication protocols. In 6th
Annual MIT Student Workshop on Computing Technology, pages 30--1, 30--2,
Salem, MA, August 1996.
Mark Smith. Formal
verification of Communication Protocols. In Reinhard Gotzhein and
Jan Bredereke, editors, Formal Description Techniques IX: Theory, Applications,
and Tools (FORTE/PSTV'96): Joint International Conference on Formal Description
Techniques for Distributed Systems and Communication Protocols, and Protocol
Specification, Testing, and Verification, Kaiserslautern, Germany, October
1996, pages 129-144. Chapman & Hall, 1996. (Abstract/Postscript)
George Varghese and Nancy A. Lynch. A tradeoff between safety and liveness
for randomized coordinated attack. Information and Computation, 128(1):57--71,
July 1996. .pdf
Mandana Vaziri. Proving correctness of a controller algorithm for the
RAID level 5 system. Master's thesis, Department of Electrical Engineering
and Computer Science, Massachusetts Institute of Technology, Cambridge,
MA 02139, August 1996.
H. B. Weinberg. Correctness of Vehicle Control Systems: A Case
Study. Master of Science Thesis, Department of Electrical
Engineering and Computer Science, Massachusetts Institute of
Technology, February 1996. Also, Technical Report MIT/LCS/TR-685,
Laboratory for Computer Science, Massachusetts Institute of
Technology. (Abstract/Postscript)
H. B. Weinberg and Nancy
Lynch. Correctness of Vehicle Control Systems - A Case
Study. Proceedings of the 17th IEEE Real-Time Systems
Symposium, pages 62-72, Washington, D. C., December, 1996. (Abstract/Postscript)
H. B. Weinberg, Nancy
Lynch, and Norman Delisle. Verification of Automated Vehicle
Protection Systems. In R. Alur, T. Henzinger, and E. Sontag,
editors, Hybrid Systems III: Verification and Control (DIMACS/SYCON
Workshop on Verification and Control of Hybrid Systems, New Brunswick,
New Jersey, October 1995), volume 1066 of Lecture Notes in Computer
Science, pages 101-113. Springer-Verlag 1996. (Abstract/Postscript)
1995
Hagit Attiya, Amotz Bar-Noy, and Danny Dolev. Sharing memory robustly
in message-passing systems. Journal of the ACM, 42(1):124--142,
January 1995.
Hagit Attiya and Sergio Rajsbaum. A combinatorial framework for wait-free
computability. Technical Report 95/3, Digital Equipment Corporation,
Cambridge Research Lab, Cambridge, MA 02139, March 1995.
Soma Chaudhuri, Maurice Herlihy, Nancy A. Lynch, and Mark R. Tuttle.
A tight lower bound for processor coordination. In Donald S. Fussell and
Miroslaw Malek, editors, Responsive Computer Systems: Steps Toward Fault-Tolerant
Real-Time Systems, chapter 1, pages 1--18. Kluwer Academic Publishers,
Boston, MA, 1995. Selected papers from the Second International Workshop
on Responsive Computer Systems Lincoln, New Hampshire, September 28-30,
1993). .ps
A. Charny, G. Leeb, and M. Clarke. Some observations on source behavior
5 of the traffic management specification. Research Report AF-TM-95-0976R1,
Digital Equipment Corporation, Littleton, Massachusetts, August 1995. Presented
at ATM Forum Traffic Management.
R. De Nicola and R. Segala. A process algebraic view of I/O automata.
Theoretical Computer Science, 138:391--423, March 1995. Also, Rapporto
Tecnico N. SI-92/05, Universita ``La Sapienza'', Rome.
Alan Fekete, Nancy Lynch, and William Weihl. Hybrid atomicity for nested
transactions. Theoretical Computer Science B (Logic, semantics and theory
of programming), 149(1):151--178, September 1995. Special issue of TCS
devoted to ICDT '92. .pdf
Alan Fekete, Frans Kaashoek and Nancy
Lynch. Implementing Sequentially-Consistent Shared Objects Using
Group and Point-to-Point Communication . In the 15th International
Conference on Distributed Computing Systems (ICDCS95), pages 439-449, Vancouver,
Canada, May/June 1995, IEEE. (Abstract/Postscript).
Also, Technical Report MIT/LCS/TM-518, Laboratory for Computer Science,
Massachusetts Institute of Technology, June 1995. (Abstract/Postscript)
H. Galeana-Sanchez and S. Rajsbaum. Cycle pancyclism in tournaments
I. Graphs and Combinatorics, 11:233--243, 1995.
Rainer Gawlick. Admission Control and Routing: Theory and Practice
Ph.D. Thesis, Department of Electrical Engineering and Computer Schence,
Laboratory for Computer Science, Massachusetts Institute of Technology,
June 1995. Also, Technical Report MIT/LCS/TR-679, Laboratory for Computer
Science, Massachusetts Institute of Technology. (Abstract/Postscript)
Rainer Gawlick, Charles Kalmanek, and K. G. Ramakrishnan. On-line routing
for permanent virtual circuits. Proceedings of IEEE INFOCOM 95: Fourteenth
Annual Joint Conference of the IEEE Computer and Communication Societies,
pages 278-288, Boston, Massachusetts, April 1995.
Maurice Herlihy and Sergio Rajsbaum. Algebraic spans. In Proceedings
of the Fourteenth Annual ACM Symposium on Principles of Distributed Computing,
pages 90--99, Ottawa, Ontario, Canada, August 1995.
M. Herlihy, B. H. Lim, and N. Shavit. Scalable concurrent counting.
ACM Transactions on Computer Systems, 13(4):343--364, 1995.
Paris Christos Kanellakis, Dimitrios Michailidis, and Alex
A. Shvartsman. Controlling Memory Access in Efficient Fault-Tolerant
Parallel Algorithms. Nordic Journal of Computing, Volume 2, pages
146-180, 1995. (Abstract/Postscript)
John Kleinberg,
Hagit Attiya and
Nancy Lynch. Trade-offs
between Message Delivery and Quiesce Times in Connection Management Protocols.
Proceedings of the Third Israel Symposium on Theory of Computing and
Systems, pages 258-267, Tel-Aviv, Israel, January 1995. (Abstract/Paper)
Victor Luchangco.
Using Simulation Techniques to Prove Timing Properties. Master
of Science Thesis, Department of Electrical Engineering and Computer Science,
Massachusetts Institute of Technology, June 1995. (Abstract/Postscript)
Victor Luchangco,
Ekrem Soylemez, Stephen Garland, and Nancy
Lynch. Verifying timing properties of concurrent algorithms.
In Dieter Hogrefe and Stefan Leue, editors, Formal Description Techniques
VII: Proceedings of the 7th IFIP WG6.1 International Conference on Formal
Description Techniques (FORTE'94, Berne, Switzerland, October 1994), pages
259--273. Chapman and Hall, 1995. (Abstract/Postscript).
Nancy Lynch. Proving performance properties (even probabilistic
ones).
In Dieter Hogrefe and Stefan Leue, editors, Formal Description Techniques
VII: Proceedings of the 7th IFIP WG6.1 International Conference on Formal
Description Techniques (FORTE'94), pages 3--20. Chapman and Hall, 1995.
Invited talk.
Nancy Lynch. Simulation techniques for proving properties of real-time
systems. In Sang H. Son, editor, Advances in Real-Time Systems,
chapter 13, pages 299--332. Prentice Hall,
