8:25 - 8:30 |
Welcome (Geoff Hamilton, Temesghen Kahsai, Maurizio Proietti) |
|
|
8:30 - 9:30 |
VPT invited talk 1: Elvira Albert (Instituto de Tecnología del Conocimiento, and Complutense University of Madrid, Spain) |
|
Superoptimization of (Optimized) Smart Contracts
|
|
(chair: Geoff Hamilton) |
|
|
|
VPT Session (chair: Geoff Hamilton)
|
9:30 - 10:00 |
Klaus Havelund |
|
Specification-based Monitoring in C++
|
|
|
10:00 - 10:30 |
Coffee Break |
|
|
10:30 - 11:30 |
VPT invited talk 2: Robert Glück (University of Copenhagen, Denmark) |
|
Principles of Reversible Computation
|
|
(chair: Maurizio Proietti) |
|
|
11:30 - 12:30 |
HCVS invited talk 1: Bruno Blanchet (INRIA, Paris, France) |
|
The security protocol verifier ProVerif and its Horn clause resolution algorithm
|
|
(chair: Maurizio Proietti) |
|
|
12:30 - 14:00 |
Lunch Break |
|
|
|
HCVS session 1 (chair: Fabio Fioravanti)
|
14:00 - 14:30 |
Elvira Albert, Miguel Isabel, Clara Rodríguez-Núñez and Albert Rubio |
|
Towards using Horn Clauses in Zero-Knowledge Protocols
|
14:30 - 15:00 |
Hossein Hojjat and Philipp Rümmer |
|
Opti-Rica: Towards an Efficient Optimizing Horn Solver
|
15:00 - 15:30 |
Leonardo Alt, Martin Blicha, Antti Hyvärinen and Natasha Sharygina |
|
SolCMC: Solidity Compiler's Model Checker (Presentation-only paper)
|
15:30 - 16:00 |
Muhammad Usama Sardar, Said Musaev and Christof Fetzer |
|
Demystifying Attestation in Intel Trust Domain Extensions via Formal Verification (Presentation-only paper)
|
|
|
16:00 - 16:30 |
Coffe Break |
|
|
16:30 - 17:30 |
HCVS invited talk 2: Aws Albarghouthi (University of Wisconsin–Madison, USA) |
|
Privacy and Automated Verification
|
|
(chair: Philipp Rümmer) |
|
|
|
HCVS Session 2 (chair: Philipp Rümmer)
|
17:30 - 18:00 |
Tewodros A. Beyene and Amit Sahu |
|
Practical Analysis of Neural Networks Using Constraints Solving
|
18:00 - 18:30 |
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti |
|
Contract Verification using Catamorphisms and Constrained Horn Clause Transformations
|
|
|
18:30 - 19:00 |
Emanuele De Angelis, Hari Govind V K |
|
CHC-COMP 2022 Report |
|
|
19:00 |
Closing |