Concurrent program verification with invariant-guided underapproximation

DOI10.1007/978-3-319-68167-2_17MaRDI QIDQ5096088zbMATH OpenOpenAlexFDO

Authors Sumanth Prabhu, Peter Schrammel, Mandayam Srivas, Michael Tautschnig, Anand Yeolekar

Publication date 12 August 2022

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL http://sro.sussex.ac.uk/69531/1/paper.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Computer Aided Verification
• Proof-Guided Underapproximation Widening for Bounded Model Checking
• An integrated specification and verification technique for highly concurrent data structures
• Verification of concurrent programs using Petri net unfoldings
• Counter-example guided program verification

Cited in

(4)

• LCTD: test-guided proofs for C programs on LLVM
• Proof-guided underapproximation-widening for multi-process systems
• Proof-Guided Underapproximation Widening for Bounded Model Checking
• Adequate proof principles for invariance and liveness properties of concurrent programs

This page was built for publication: Concurrent program verification with invariant-guided underapproximation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5096088)