Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol.
Alexei LisitsaPublished in: WING@ETAPS/IJCAR (2010)
Keyphrases
- mutual exclusion
- long distance
- cryptographic protocols
- protocol specification
- formal analysis
- model checker
- model checking
- formal proof
- test bed
- planning domains
- lightweight
- temporal planning
- formal verification
- moment invariants
- temporal logic
- case study
- authentication protocol
- colored petri nets
- petri net
- security protocols
- formal methods
- tcp ip
- affine invariant
- search strategies