[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Why Amazon Chose TLA+
Would it be possible to get the source code of TLA+ models you mentioned in the paper?
I am a PhD candidate from University of Illinois. I have worked with VCC in various contexts. (E.g, http://dx.doi.org/10.1145/2666356.2594325)
I would like to explore ways to prove your code correct using VCC (or other automated deductive techniques).
On Thursday, June 12, 2014 2:50:21 PM UTC-5, Chris Newcombe wrote:
> The following paper was presented at ABZ'2014 last week, and is now available in the conference proceedings:
> C., Why Amazon Chose TLA+, in
> Abstract State Machines, Alloy, B, TLA, VDM, and Z Lecture Notes in
> Computer Science Volume 8477, 2014, pp 25-39;
> http://link.springer.com/chapter/10.1007%2F978-3-662-43652-3_3 ;
> I'm happy to provide copies privately on request.
> The above is a partner to our other paper, "Use of Formal Methods at Amazon Web Services", which is currently available via the TLA+ home page. See earlier post: https://groups.google.com/d/msg/tlaplus/bPlvP1V5hyk/0xPGIrpb7wUJ