SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions | Zendy

Anil Madhavapeddy | Zendy; David Scott | Zendy; Richard R. Sharp | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions

Author(s) -

Anil Madhavapeddy,

David Scott,

Richard R. Sharp

Publication year - 2005

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-28195-9

DOI - 10.1007/11537328_23

Subject(s) - computer science , model checking , artifact (error) , abstraction , programming language , software engineering , software , theoretical computer science , artificial intelligence , philosophy , epistemology

Conventional software model-checking involves (i) creating an abstract model of a complex application; (ii) validating this model against the application; and (iii) checking safety properties against the abstract model. To non-experts, steps (i) and (ii) are often the most daunting. Firstly how does one decide which aspects of the application to include in the abstract model? Secondly, how does one determine whether the abstraction inadvertently “hides” critical bugs? Similarly, if a counter-example is found, how does one determine whether this is a genuine bug or just a modelling artifact?

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research