Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
SpaceSearch: a library for building and verifying solver-aided tools
Proceedings of the ACM on Programming Languages (PACMPL), Volume 1, Issue ICFPArticle No.: 25, Pages 1–28https://doi.org/10.1145/3110269Many verification tools build on automated solvers. These tools reduce problems in a specific application domain (e.g., compiler optimization validation) to queries that can be discharged with a highly optimized solver. But the correctness of the ...
- ArticleJuly 2013
Verification condition generation for permission logics with abstract predicates and abstraction functions
ECOOP'13: Proceedings of the 27th European conference on Object-Oriented ProgrammingJuly 2013, Pages 451–476https://doi.org/10.1007/978-3-642-39038-8_19Abstract predicates are the primary abstraction mechanism for program logics based on access permissions, such as separation logic and implicit dynamic frames. In addition to abstract predicates, it is useful to also support classical abstraction ...