Modular Total Correctness Verification of Fine-Grained Concurrent Programs with Exceptions and I/O
Many powerful higher-order logics have been proposed for the modular specification and verification of fine-grained concurrent imperative programs. In this talk, I present a logic that is fairly close to what my VeriFast modular verification tool for C and Java implements. To achieve higher-order-ishness (higher-order assertions, nested Hoare triples, storing assertions in the heap, etc.), a relatively simple approach is followed: assertion lambda applications and nested triples may occur only in positive positions. Negative facts can be passed around in the form of lemma lambdas, i.e. ghost command lambdas. We prove termination of such higher-order ghost code using call permissions, a technique we are presenting at ECOOP 2015 this summer. I will also discuss the problem of provably live exception handling (FTfJP 2015), and modular verification of interactive behavior (ESOP 2014).
Speaker Details
Since finishing my PhD in 2007 and a postdoc in 2010 at the Department of Computer Science of KU Leuven – University of Leuven, Belgium, both under Prof. Frank Piessens, I have been an assistant professor at the same department. My research interests are centered around modular formal verification of imperative programs. I learned the ropes in this field during a total of three extremely fun and fruitful internships at MSR Redmond in 2004 and 2005, working with Wolfram Schulte, Rustan Leino, Mike Barnett and others on Spec# and Boogie.
- Series:
- Microsoft Research Talks
- Date:
- Speakers:
- Bart Jacobs
- Affiliation:
- University of Leuven
-
-
Jeff Running
-
Series: Microsoft Research Talks
-
-
-
-
Galea: The Bridge Between Mixed Reality and Neurotechnology
Speakers:- Eva Esteban,
- Conor Russomanno
-
Current and Future Application of BCIs
Speakers:- Christoph Guger
-
Challenges in Evolving a Successful Database Product (SQL Server) to a Cloud Service (SQL Azure)
Speakers:- Hanuma Kodavalla,
- Phil Bernstein
-
Improving text prediction accuracy using neurophysiology
Speakers:- Sophia Mehdizadeh
-
-
DIABLo: a Deep Individual-Agnostic Binaural Localizer
Speakers:- Shoken Kaneko
-
-
Recent Efforts Towards Efficient And Scalable Neural Waveform Coding
Speakers:- Kai Zhen
-
-
Audio-based Toxic Language Detection
Speakers:- Midia Yousefi
-
-
From SqueezeNet to SqueezeBERT: Developing Efficient Deep Neural Networks
Speakers:- Sujeeth Bharadwaj
-
Hope Speech and Help Speech: Surfacing Positivity Amidst Hate
Speakers:- Monojit Choudhury
-
-
-
-
-
'F' to 'A' on the N.Y. Regents Science Exams: An Overview of the Aristo Project
Speakers:- Peter Clark
-
Checkpointing the Un-checkpointable: the Split-Process Approach for MPI and Formal Verification
Speakers:- Gene Cooperman
-
Learning Structured Models for Safe Robot Control
Speakers:- Ashish Kapoor
-
-