[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

Hoffman08b

  1. Leah Hoffman
  2. Talking Model-checking Technology
  3. =INTERVIEW HISTORY MODEL CHECKING VERIFICATION FSM TEMPORAL LOGIC
  4. Commun ACM V51n7(Jul 2008)pp112+110-111
  5. Interview with Turing prize winners E Allen Emerson & Edmund M Clark & Joseph Sifakis
  6. Painful birth: theoretically trivial and practically impossible!
  7. Handle programs that do not stop. Avoid humans proving programs. Based on finite state abstractions of program+hardware and requirements specified in temporal logic. If property is not satisfied by abstraction then procedure gives a diagnostic trace of the bad behavior.
  8. Problem: State Explosion: no of cases to consider can grow exponentially with the size of the model.
  9. Benefits: precise specifications.
  10. Limits: 10^100 states!
  11. Microsoft has one used for device drivers!

Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]