Monotonicity in shared-memory program verification

Thesis

Predicate abstraction is a key enabling technology for applying model checkers to programs written in mainstream languages. It has been used very successfully for debugging sequential system-level C code. Although model checking was originally designed for analysing concurrent systems, there is little evidence of fruitful applications of predicate abstraction to shared-variable concurrent software. The goal of the present thesis is to close this gap. We propose an algorithmic solu...

Expand abstract

Authors: Kaiser, A

• Publication date: 2013
• DOI: 10.5287/ora-jv2yqrpzq
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: concurrency; monotonicity; well quasi-ordered systems; predicate abstraction; parameterized model checking
• Subjects: Computer science (mathematics); Theory and automated verification; Program development and tools; Scalable systems