2015/11/03 by Radu I. Siminiceanu, Ijaz Ahmed, Siminiceanu, Radu +3
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Security and Verification in Computing
paper · doi:10.14279/tuj.eceasst.53.790
openalex publication_date 2024/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
We propose an approach to formally verify Plural specifications of concurrent programs based on access permissions and typestates, by model-checking automatically generated abstract state-machines. Our approach captures all possible relevant behaviors of abstract concurrent programs implementing the specification. We describe the formal methodology employed in our technique and provide an example as proof of concept for the state-machine construction rules. We implemented the fully automated algorithm to generate and verify models as a freely available plug-in of the Plural tool, called Pulse. We tested Pulse on the full specification of a Multi Threaded Task Server commercial application and showed that this approach scales well and is efficient in finding errors in specifications that could not be previously detected with the Data Flow Analysis (DFA) capabilities of Plural.