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


Announcements

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