Group colloquium: Specification & Verification of Message-Passing Parallel Programs

When: March 14, 2019, 15:45-16:30

Where: Ravelijn 2503

Who: Stephen Siegel

Recent years have witnessed steady progress in the field of formal program verification. The development of the ACSL specification language, for example, has enabled the logically precise specification of behavioral contracts for sequential C programs, and the Frama-C platform has enabled the deductive verification of those contracts. Symbolic execution provides another approach to the problem. We are now exploring ways to extend these approaches to parallel, message-passing C programs. The first step is to develop a precise semantics of a contract for a procedure executed by multiple concurrent processes. We can then postulate extensions to ACSL that capture the semantics. Finally, we show how deductive and symbolic execution techniques can be used to verify such contracts.

[Joint work with Ziqing Luo, University of Delaware]

	Home > News and Events > Events
<< EEMCS (EWI) Home News and Events » Group Colloquium » Events » In the Media People Research Education Vacancies Intranet Contact	Group colloquium: Specification & Verification of Message-Passing Parallel Programs When: March 14, 2019, 15:45-16:30 Where: Ravelijn 2503 Who: Stephen Siegel Recent years have witnessed steady progress in the field of formal program verification. The development of the ACSL specification language, for example, has enabled the logically precise specification of behavioral contracts for sequential C programs, and the Frama-C platform has enabled the deductive verification of those contracts. Symbolic execution provides another approach to the problem. We are now exploring ways to extend these approaches to parallel, message-passing C programs. The first step is to develop a precise semantics of a contract for a procedure executed by multiple concurrent processes. We can then postulate extensions to ACSL that capture the semantics. Finally, we show how deductive and symbolic execution techniques can be used to verify such contracts. [Joint work with Ziqing Luo, University of Delaware]