Question

Per their Gödel prize citation, Brooks and O’Hearn simultaneously solved the two major challenges of handling this data type and concurrency by developing CSL. In separation logic, the right arrow binary operator makes an assertion about an object with this data type; more generally, separation logic was created to improve on Hoare logic’s difficulty with manipulating and reasoning about this data type. Reasoning about data structures is aided by diagrams consisting of pairs of squares called “box-and-[this word] diagrams”. (15[1])Formal verification of programs using this data type is harder because of (*) aliasing, (10[1])a phenomenon (10[1])where two objects of this type overlap. Every individual node (-5[1])in a linked list contains some data along with an object of this type. For 10 points, dynamic memory allocation returns an object of what data type that references a location in the heap? ■END■ (10[1])

Back to tossups