Constraint Languages for Parameterized Verification
Giorgio
Delzanno
Dipartimento
di Informatica e Scienze dell’Informazione
Universita' di Genova
·
Computation Tree Logic and
Model Checking
References:
o
Model Checking
[Clarke-Grumberg-Peled ]
o A Model Checking Tutorial
[Merz]
·
Constraint-based
Model Checking
References:
o Symbolic model checking with rich assertional languages
[Kesten-Maler-Marcus-Pnueli-Shahar 97]
o
Algorithmic
Analysis of Programs with Well Quasi-Ordered Domains
[Abdulla-Cerans-Jonsson-Tsay I&C ‘00]
o
Ensuring Completeness of Symbolic Verification Methods for
Infinite-State Systems
[Abdulla-Jonsson TCS ‘01]
o
Well-structured Transition Systems Everywhere
[Finkel-Schnoebelen TCS ‘01]
o Comparing the
Expressive Power of Well-structured Transition Systems
[Abdulla-Delzanno-Van Begin CSL ‘07]
·
Verification of
Parameterized Systems (broadcast communication)
·
Approximated
Verification Parameterized Systems (for different topologies)
References:
o Verification of Cache
coherence protocols
o Approximated parameterized
verification of infinite-state processes with global conditions
o Handling Parameterized
Systems with Non-Atomic Global Conditions
o Parameterized Verification of Ad Hoc Networks