Topics in Verification

Research Directions in Concurrency (Winter 2011)

Categories and papers:

Rely-Guarantee and compositional reasoning (2)

* In transition from global to modular temporal reasoning about programs. A. Pnueli
Specification and Design of (parallel) programs, Cliff B. Jones

The rely-guarantee method for verifying shared variable concurrent programs

Learning Assumptions for Compositional Verification
Proof rules for automated compositional verification true learning
An explanatory presentation of composition rules for assumption-commitment specifications

Static Compositional Reasoning (1-2)

- Heap decomposition for concurrent shape analysis
Scalable Shape Analysis for Systems Code
Efficiently inferring thread co-relations

True Concurrency: Petri nets, Traces, Event Structures (1-2)

Petri nets and other models of concurrency
Petri nets, event structures and domains
Introduction to Trace Thoery
+Regular Traces and Event Structures

Net Unfoldings (1)

- A technique of state space search based on unfolding
- An improvement of McMillan's unfolding algorithm
A false history of true concurrency

Concurrent Reachability (1-2)

A generic approach to the static analysis of concurrent programs with procedures
Context-bounded model checking of concurrent software
Context-bounded analysis of concurrent programs with dynamic thread creation
Bounded Underapproximations

SMT Encodings (1)

- Static and precise detection of concurrency errors in systems code using SMT solvers
On interference abstractions

Modular Reasoning (1)

- Thread-modular verification for shared-memory programs
Local proofs for global safety properties

New models of shared memory (1)

- Concurrent programming with revisions and isolation types
- Transactional Memory

Testing (1-2)

- FastTrack: efficient and precise dynamic race detection
Hybrid data race detection
A randomized scheduler with probabilistic guarantees for finding bugs
Effective data-race detection for the kernel


Lectures are held on Mondays at 2-4pm in BA 3000.