| Autor: | Zohar Manna, Michael Colón, Tomás E. Uribe, Nikolaj Bjørner, Henny B. Sipma, Anca Browne, Bernd Finkbeiner |
|---|---|
| Rok vydání: | 2000 |
| Předmět: |
Model checking
High-level verification Theoretical computer science Functional verification Computer science Programming language Runtime verification computer.software_genre Theoretical Computer Science Hardware and Architecture Computer Science::Logic in Computer Science Temporal logic Mutual exclusion Formal verification computer Software |
| Zdroj: | Formal Methods in System Design. 16:227-270 |
| ISSN: | 0925-9856 |
| DOI: | 10.1023/a:1008700623084 |
| Popis: | We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verify the classic two-process algorithm and simple variants, as well as an atomic parameterized version. The methods used include deductive verification rules, verification diagrams, automatic invariant generation, and finite-state model checking and abstraction. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink