Verifying Parameterized taDOM+ Lock Managers

DOI10.1007/978-3-540-77566-9_40MaRDI QIDQ5448673zbMATH OpenOpenAlexFDO

Authors Antti Siirtola, Michal Valenta

Publication date 7 March 2008

Published in SOFSEM 2008: Theory and Practice of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-77566-9_40

zbMATH Keywords

model checkingcase studyVerificationXML databasesparameterized systems

Mathematics Subject Classification ID

Database theory (68P15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Monotonic Abstraction in Action
• scientific article; zbMATH DE number 1796121
• Handling Parameterized Systems with Non-atomic Global Conditions
• Transformational Verification of Parameterized Protocols Using Array Formulas
• Model checking transactional memories

Cites work

• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 1956578 (Why is no real title available?)
• scientific article; zbMATH DE number 2102714 (Why is no real title available?)
• A structural induction theorem for processes
• An approach to automating the verification of compact parallel coordination programs. I
• Appendix
• Automatic verification of parameterized networks of processes
• Computer Science Logic
• Defining liveness
• Exact and efficient verification of parameterized cache coherence protocols
• Introduction to algorithms
• Reasoning about systems with many processes

This page was built for publication: Verifying Parameterized taDOM+ Lock Managers

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