Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Publication
Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
We describe a decision procedure for a logic that supports 1) finite collections of elements (sets or multisets), 2) the cardinality operator, 3) a total order relation on elements, and 4) min and max operators on entire collections. Among the applications of this logic are 1) reasoning about the externally observable behavior of data structures such as random access priority queues, 2) specifying witness functions for synthesis problems of set algebra, and 3) reasoning about constraints on orderings arising in termination proofs.
Pandula Manura Liyanage, Claudia Cancellieri, Giacomo Lorenzin