[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Leah Hoffman
- Talking Model-checking Technology
- =INTERVIEW HISTORY MODEL CHECKING VERIFICATION FSM TEMPORAL LOGIC
- Commun ACM V51n7(Jul 2008)pp112+110-111
- Interview with Turing prize winners E Allen Emerson & Edmund M Clark & Joseph Sifakis
- Painful birth: theoretically trivial and practically impossible!
- 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.
- Problem: State Explosion: no of cases to consider can grow exponentially with the size of the model.
- Benefits: precise specifications.
- Limits: 10^100 states!
- Microsoft has one used for device drivers!
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]