Name
Abstract | ||
|---|---|---|
ProB is an animation and model checking tool for the B Method, which can deal with many interesting specifications. Some specifications, however, contain complicated functions which cannot be represented explicitly by a tool. We present a scheme with which higher-order recursive functions can be encoded in B, and establish soundness of this scheme. We then describe a symbolic representation for such functions. This representation enables ProB to successfully animate and model check a new class of relevant specifications, where animation is especially important due to the involved nature of the specification. |
Year | Venue | Keywords |
|---|---|---|
2009 | Rigorous Methods for Software Construction and Analysis | symbolic representation,complicated function,higher-order recursive function,model checking tool,recursive function,new class,interesting specification,involved nature,relevant specification,b method,model checking,higher order |
Field | DocType | Volume |
Model checking,Computer science,Theoretical computer science,B-Method,Animation,Soundness,Logic programming,Recursive functions | Conference | 5115 |
ISSN | ISBN | Citations |
0302-9743 | 3-642-11446-6 | 2 |
PageRank | References | Authors |
0.47 | 12 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Leuschel | 1 | 2156 | 135.89 |
| Dominique Cansell | 2 | 254 | 21.29 |
| Michael Butler | 3 | 1768 | 104.74 |