Observable Confluence for Constraint Handling Rules

2007 ◽  
pp. 224-239 ◽  
Author(s):  
Gregory J. Duck ◽  
Peter J. Stuckey ◽  
Martin Sulzmann
Keyword(s):  
Constraint Handling

Deep generative model for non-convex constraint handling

2020 ◽  
Author(s):  
Naoki Sakamoto ◽  
Eiji Semmatsu ◽  
Kazuto Fukuchi ◽  
Jun Sakuma ◽  
Youhei Akimoto
Keyword(s):  
Generative Model ◽  
Constraint Handling ◽  
Convex Constraint

scholarly journals Shape Neutral Analysis of Graph-based Data-structures

2018 ◽  
Vol 18 (3-4) ◽  
pp. 470-483 ◽  
Author(s):  
GREGORY J. DUCK ◽  
JOXAN JAFFAR ◽  
ROLAND H. C. YAP
Keyword(s):  
Data Structure ◽  
Data Structures ◽  
Program Analysis ◽  
Constraint Handling ◽  
C Programs ◽  
Wide Range ◽  
Target Program ◽  
Target Data ◽  
Structure Graph ◽  
Structure Properties

AbstractMalformed data-structures can lead to runtime errors such as arbitrary memory access or corruption. Despite this, reasoning over data-structure properties for low-level heap manipulating programs remains challenging. In this paper we present a constraint-based program analysis that checks data-structure integrity, w.r.t. given target data-structure properties, as the heap is manipulated by the program. Our approach is to automatically generate a solver for properties using the type definitions from the target program. The generated solver is implemented using a Constraint Handling Rules (CHR) extension of built-in heap, integer and equality solvers. A key property of our program analysis is that the target data-structure properties are shape neutral, i.e., the analysis does not check for properties relating to a given data-structure graph shape, such as doubly-linked-lists versus trees. Nevertheless, the analysis can detect errors in a wide range of data-structure manipulating programs, including those that use lists, trees, DAGs, graphs, etc. We present an implementation that uses the Satisfiability Modulo Constraint Handling Rules (SMCHR) system. Experimental results show that our approach works well for real-world C programs.

Sign in / Sign up

Export Citation Format

Share Document