2LS: Heap Analysis and Memory Safety
Viktor Malík, Peter Schrammel, Tomáš Vojnar · Lecture notes in computer science · 2020
Abstract 2LS is a framework for analysis of sequential C programs based on the CPROVER infrastructure and template-based synthesis techniques for checking both safety and termination. The paper presents the main improvements done in 2LS since 2018, which concern mainly the way 2LS handles dynamically allocated objects and structures as well as combinations of abstract domains.