The words contained in this file might help you see if this file matches what you are looking for:

...Logic verification of ansi c code with spin gerard j holzmann bell laboratories lucent technologies murray hill new jersey usa research labs com abstract we describe a tool called ax that can be used in combination the model checker to efficiently verify logical properties distributed software systems implemented standard short for automaton extractor extract models from at user defined level abstraction target applications include telephone switching operating protocol implementations con currency control methods and client server this paper discusses how is currently plan extend it was formal two substantial soft ware commercial checkpoint management system call processing switch introduction construction reliable has long been an elusive goal well known general even simple such as program termination or deadlock are formally undecidable efforts development mechanical therefore usually concen trate on carefully subsets programs instance obtained by imposing syntactic restrictions pro...