Verification, Interaction and Proofs

VIP (Verification, Interaction and Proofs) is a French - Chinese research project involving

• INRIA Paris, pir2 team at IRIF, Paris
• State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Science, Beijing

Its scientific program is built upon a cross-fertilization of a culture of verification (with automata theory as a main conceptual framework) and a culture of proofs and programs.

Its main themes are

• Verification (linearizability, verification of data structures, program verification techniques).
• Complex systems and theories of interaction (general theory of interaction, structural information theory, concurrency, causal models of computation).
• Deductive methods and formal proofs (bridging finite and infinite proofs, bridging saturation and cut-elimination, readable formal proofs of algorithms).

Our first meeting will take place in Paris, at the IRIF laboratory, University Paris Diderot on November 19 - 23.

Registration is free but mandatory. If you wish to attend, please fill in this form before November 10th, 2018.

For any question or request, please send an email to both organizers Thomas Ehrhard and Jean Krivine.

The program of the formal part of the meeting (Nov 19-21) can be found here. The registered speakers are:

• Giovanni Bernardi, IRIF: On usable clients
• Ahmed Bouajjani, IRIF: Robustness against asynchrony
• Gilles Dowek, LSV: Decidability, Introduction Rules, and Automata
• Amina Doumane, LIP: Completeness for Identity-free Kleene Lattices
• Thomas Ehrhard, IRIF: On the denotational semantics of LL with least and greatest fixpoints
• Constantin Enea, IRIF: Specifying and Verifying Concurrent Objects
• Ying Jiang, ISCAS: Towards Combining Model Checking and Proof Checking
• Jean Krivine, IRIF: A Calculus of Branching Processes
• Jean-Jacques Lévy, IRIF: Comparing a formal proof in Why3, Coq and Isabelle
• Bin Li, Fudan university: The Binary Space Partitioning-Tree Process
• Yi Lv, ISCAS: Dynamic Verification of Java Memory Model with Static Analysis
• Jean-François Monin, VERIMAG: TBA
• Jun Pang, University of Luxembourg: Understanding and Control Long-run Dynamics of Large Biological Networks
• Mihaela Sighireanu, IRIF: Separation Logic for Static Analysis of Dynamic Memory Allocators
• Yong Wang, AMSS: Causal regulatory network inference for understanding genetic variants
• Peng Wu, ISCAS: Diversity Driven Adaptive Testing of Concurrent Programs
• Zhilin Wu, ISCAS: Android Stack Machine
• Rongjie Yan, ISCAS: Design Verification and Validation for Reliable Safety-critical Autonomous Control Systems
• Qian Zhang, Singapore Management University: Modelling and Analysis for Network Security - an Algebraic Approach
• Wenhui Zhang, ISCAS: Bounded Correctness

Talk proposal submissions for the informal part of the meeting (Nov 22-24) are still welcome, please use this form

The social dinner will take place on a French restaurant located on a Chinese junk Boat on the river Seine. Participation is free for the members of the VIP project and for invited speakers, and is charged 35 euros per additional diners. All participants need to indicate whether they wish to attend to the event on the registration form. There is a limited number of seats, they will be allocated on a first come first served basis.

Last update: 2018-10-29