%0 Journal Article %1 Win03usingsimulated %A Win, Toh Ne %A Ernst, Michael D. %A Garland, Stephen J. %A Kirli, Dilsun %A Lynch, Nancy A. %D 2003 %J Software Tools for Technology Transfer %K automated concurrent ioautomata paxos proof simulation %P 283--297 %T Using Simulated Execution in Verifying Distributed Algorithms %U http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.4897 %V 6 %X This paper presents a methodology for proving properties of distributed systems in which simulated execution assists and enhances formal proofs. It is well known that techniques such as testing can increase con dence in an implementation, but cannot by themselves demonstrate correctness. In addition to detecting simple errors quickly and to providing intuition about behavior, execution-based techniques can also reveal unexpected properties, suggest necessary lemmas, and provide information to structure proofs. This paper also describes the use of these techniques in a machine-checked proof of correctness of the Paxos algorithm for distributed consensus.

@article{Win03usingsimulated, abstract = {This paper presents a methodology for proving properties of distributed systems in which simulated execution assists and enhances formal proofs. It is well known that techniques such as testing can increase con dence in an implementation, but cannot by themselves demonstrate correctness. In addition to detecting simple errors quickly and to providing intuition about behavior, execution-based techniques can also reveal unexpected properties, suggest necessary lemmas, and provide information to structure proofs. This paper also describes the use of these techniques in a machine-checked proof of correctness of the Paxos algorithm for distributed consensus.}, added-at = {2009-11-13T18:20:20.000+0100}, author = {Win, Toh Ne and Ernst, Michael D. and Garland, Stephen J. and Kirli, Dilsun and Lynch, Nancy A.}, biburl = {https://www.bibsonomy.org/bibtex/2dc586742d417284af6082b1d6bcdc6df/giuliano.losa}, description = {Using Simulated Execution in Verifying Distributed Algorithms}, interhash = {d03a27d3a4a146f7bb3fdb8bf9b408d6}, intrahash = {dc586742d417284af6082b1d6bcdc6df}, journal = {Software Tools for Technology Transfer}, keywords = {automated concurrent ioautomata paxos proof simulation}, pages = {283--297}, timestamp = {2010-01-29T00:24:49.000+0100}, title = {Using Simulated Execution in Verifying Distributed Algorithms}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.4897}, volume = 6, year = 2003 }