Conference item icon

Conference item

The Spotlight Principle

Abstract:

Formal verification of safety and liveness properties of systems with a dynamically changing, unbounded number of interlinked processes and infinite-domain local data is challenging due to the two sources of infiniteness. The existing state abstraction-based approaches Data Type Reduction and Environment Abstraction each address one aspect, but the former doesn’t support infinite-domain local data and the latter doesn’t support links and is restricted to particular properties. The contributio...

Expand abstract

Actions


Access Document


Files:

Authors


Björn Wachter More by this author
Bernd Westphal More by this author
Publisher:
Springer
Volume:
4349
Publication date:
2007
URN:
uuid:103e548a-a0df-4214-9f0b-3dbecc14fc06
Local pid:
cs:4919
ISBN:
978-3-540-69735-0

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP