Abstract Diagnosis for tccp using a Linear Temporal Logic. Issue 4 (21st July 2014)

• Record Type: Journal Article
• Authors: COMINI, MARCO; TITOLO, LAURA; VILLANUEVA, ALICIA; Leuschel, Michael; Schrijvers, Tom
• Is Part Of: Theory and practice of logic programming. Volume 14:Issue 4/5(2014)
• Page Start: 787
• Page End: 801
• Publication Date: 2014-07-21
• Subjects: Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068414000349
• Languages: English
• ISSNs: 1471-0684

Abstract

<abstract abstract-type="normal"> <title>Abstract</title> <p>Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge.</p> <p>In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is <italic>valid</italic> w.r.t. a <italic>tccp</italic> program. Our proposal (based on abstract interpretation techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.</p> </abstract>