Invited tutorial

Sriram K. Rajamani (Microsoft Research, Redmond, USA)

Title: Model Checking, Abstraction and Symbolic Execution for Software

Abstract: Over the past few years, there has been growing interest in using techniques such as automatic abstraction, symbolic execution, compiler-style dataflow analysis, model checking, and abstraction-refinement to prove properties about programs written in common programming languages like C.

I will describe our experiences from two projects in this area: (1) SLAM, a checker for control intensive properties of sequential C programs, and (2) Zing, a checker for detecting concurrency errors in concurrent object-oriented programs.

(SLAM is joint work with Tom Ball, Byron Cook, Vlad Levin, Jakob Lichtenberg, Andreas Podelski and several summer-interns and visitors to MSR. Zing is joint work with Tony Andrews, Shaz Qadeer, Jakob Rehof, Madan Musuvathi and several summer-interns at MSR)


Panoram de Paris 360

Contact: Radhia[point]Cousot[arobase]polytechnique [point]fr
Last modified: Saturday May 22, 2010
Valid XHTML 1.1! Valid CSS!
ACM

VMCAI'05

Conference venue Invited speakers Invited tutorial Program Call for papers Committees Registration Sponsors Publication LNCS 3385

Affiliated events

Industrial Day NSAD'05 AIOOL'05

Paris

Accommodations Subway (map, itinary,...) Weather Maps

Links

VMCAI'04VMCAI'03
EAPLS