| 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 |