Simulating reachability using first-order logic with applications to verification of linked data structures

Simulating reachability using first-order logic with applications to verification of linked data structures

This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating of pointer-valued structure fields. One of the main obstacles is specifying and proving the...

Full description

Bibliographic Details
Main Authors: Tal Lev-Ami, Neil Immerman, Thomas Reps, Mooly Sagiv, Siddharth Srivastava, Greta Yorsh
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2009-05-01
Series:Logical Methods in Computer Science
Subjects:
computer science - logic in computer science
computer science - programming languages
f.3.1
f.3.2
f.4.1
Online Access:https://lmcs.episciences.org/680/pdf

Internet

https://lmcs.episciences.org/680/pdf

Similar Items