| 
|
QuoteRef: holzGJ5_1997
topics >
all references >
ThesaHelp:
references g-h
Group:
program proving
Topic:
model checker
Topic:
logic
Topic:
logic programming
Topic:
state machine
Topic:
theorem proving systems
Reference
Holzmann, G.J., "The model checker SPIN", IEEE Transactions on Software Engineering, 23, 5, May 1997, pp. 279-295. Google
Notes
Bang, K-S, Choi, J-Y, Yoo, C., Comments on "The Model Checker SPIN", IEEE Transactions on Software Engineering, 27.6:573-576 June 2001.
279 ;;Quote: use SPIN for design and verification of asynchronous process systems using rendezvous, buffered channels, and/or shared variables; design with PROMELA
279+;;Quote: SPIN represents correctness claims in linear temporal logic (LTL)
282 ;;Quote: SPIN uses partial order reductions that preserve the correctness property; 10-90% space and saving
282+;;Quote: used the theorem prover HOL to prove the correctness of SPIN's partial order reduction
283 ;;Quote: safety properties such as deadlock and assertions have linear cost in number of reachable states
283+;;Quote: liveness properties such as starvation and acceptance cycles take same memory and twice as much time as safety properties
ThesaHelp: references g-h (299 items)
Group: program proving (10 topics, 311 quotes)
Topic: model checker (49 items)
Topic: logic (84 items)
Topic: logic programming (34 items)
Topic: state machine (67 items)
Topic: theorem proving systems (20 items)