2021/10/05 by Eduard Kamburjan, Kamburjan, Eduard, Nathan Wasser +1
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2110.01964
openalex publication_date 2021/10/05 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
We present a novel and well automatable approach to formal verification of\nprograms with underspecified semantics, i.e., a language semantics that leaves\nopen the order of certain evaluations. First, we reduce this problem to\nnon-determinism of distributed systems, automatically extracting a distributed\nActive Object model from underspecified, sequential C code. This translation\nprocess provides a fully formal semantics for the considered C subset. In the\nextracted model every non-deterministic choice corresponds to one possible\nevaluation order. This step also automatically translates specifications in the\nANSI/ISO C Specification Language (ACSL) into method contracts and object\ninvariants for Active Objects. We then perform verification on the specified\nActive Objects model. For this we have implemented a theorem prover Crowbar\nbased on the Behavioral Program Logic (BPL), which verifies the extracted model\nwith respect to the translated specification and ensures the original property\nof the C code for all possible evaluation orders. By using model extraction, we\ncan use standard tools, without designing a new complex program logic to deal\nwith underspecification. The case study used is highly underspecified and\ncannot be verified with existing tools for C.\n