Sun 15 Nov 2020 15:40 - 16:00 at SPLASH-I - S-5 Chair(s): Davide Ancona, Eli Tilevich
Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule for concurrency. In this paper, we develop a new proof calculus for the C11 RAR memory model (a fragment of C11 with both relaxed and release-acquire accesses) that allows all Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. Our proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. We demonstrate the utility of our proof calculus by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in the theorem prover
Sun 15 Nov Times are displayed in time zone: Central Time (US & Canada) change
15:00 - 16:20: S-5Research Papers at SPLASH-I +12h Chair(s): Davide AnconaDIBRIS, University of Genova, Italy, Eli TilevichVirginia Tech | |||
15:00 - 15:20 Talk | Model-View-Update-Communicate: Session Types meet the Elm Architecture Research Papers Simon FowlerUniversity of Glasgow Link to publication DOI Pre-print Media Attached | ||
15:20 - 15:40 Talk | Putting Randomized Compiler Testing into Production Research Papers Link to publication DOI Media Attached | ||
15:40 - 16:00 Talk | Owicki-Gries Reasoning for C11 RAR Research Papers Sadegh DalvandiUniversity of Surrey, Simon DohertyUniversity of Sheffield, Brijesh DongolUniversity of Surrey, Heike WehrheimPaderborn University Link to publication DOI Media Attached | ||
16:00 - 16:20 Talk | Test-Case Reduction via Test-Case Generation: Insights From the Hypothesis Reducer Research Papers Link to publication DOI Media Attached |
Mon 16 Nov Times are displayed in time zone: Central Time (US & Canada) change
03:00 - 04:20: S-5Research Papers at SPLASH-I Chair(s): Davide AnconaDIBRIS, University of Genova, Italy, Jeremy GibbonsDepartment of Computer Science, University of Oxford | |||
03:00 - 03:20 Talk | Model-View-Update-Communicate: Session Types meet the Elm Architecture Research Papers Simon FowlerUniversity of Glasgow Link to publication DOI Pre-print Media Attached | ||
03:20 - 03:40 Talk | Putting Randomized Compiler Testing into Production Research Papers Link to publication DOI Media Attached | ||
03:40 - 04:00 Talk | Owicki-Gries Reasoning for C11 RAR Research Papers Sadegh DalvandiUniversity of Surrey, Simon DohertyUniversity of Sheffield, Brijesh DongolUniversity of Surrey, Heike WehrheimPaderborn University Link to publication DOI Media Attached | ||
04:00 - 04:20 Talk | Test-Case Reduction via Test-Case Generation: Insights From the Hypothesis Reducer Research Papers Link to publication DOI Media Attached |