The AVM is a meeting on current problems in formal verification. The goal of the meeting is to bring together researchers from the region to update each other on their research, to have time for discussion, also on possible collaborations. The meeting is open to the public.
AVM 2013 will take place at Fondazione Bruno Kessler (FBK) in Trento, Italy, from May 27th to May 29th, 2013.
AVM will take place at the Scientific and Technological Hub of FBK.
Address:
Fondazione Bruno Kessler (FBK)
Center for Scientific and Technological Research
Via Sommarive, 18
I-38123 Trento, Italy
tel. (+39) 0461 314 444
More information about past and future Alpine Verification Meetings are available on the AVM web site.
General Info:
Start Date: 27 May 2013
Start Time: 11:30
End Date: 29 May 2013
End Time: 20:00
Location: AVM will take place at the Scientific and Technological Hub of FBK.
Programme:
The program will consist of:- Two invited talks, by:
- Andrey Rybalchenko (Microsoft Research and TU Munich), and
- Roberto Sebastiani (Univ. of Trento);
- A number of presentations given by Ph.D. students;
- An "alpine" social event.
Monday (May 27th)
| 14.00 - 15.00 | Invited Talk: Roberto Sebastiani (Univ. of Trento) SMT: from Satisfiability to Optimization |
| Session 1 | |
| 15.00 - 15.30 | Adrian Beer (Univ. of Konstanz) Quantitative Analysis of Non-Deterministic System Architectures Slides |
| 15.30 - 16.00 | Shashank Pathak (Univ. of Genova) Verification and Repair of Control Policies in Robots Learning by Reinforcement |
| Break | |
| Session 2 | |
| 16.30 - 17.00 | Andrei Dan (ETH Zurich) Predicate Abstraction for Relaxed Memory Models |
| 17.00 - 17.30 | Andreas Stahlbauer (Univ. of Passau) Reusing Precisions for Efficient Regression Verification |
| 17.30 - 18.00 | Francesco Alberti (USI Lugano) Lazy Abstraction with Interpolants for Arrays |
| 18.00 - 18.30 | Ayoub Nouri (Verimag) Towards an Integrated Approach for Performance Evaluation of Embedded System: Statistical Model Checking and Learning-Based Abstraction |
Tuesday (May 28th)
| 09.00 - 10.00 | Invited Talk: Andrey Rybalchenko (Microsoft Research and TU Munich) Solving Quantified Horn Clauses |
| Break | |
| Session 3 | |
| 10.30 - 11.00 | Tewodros A. Beyene (TU Munich) Solving Existentially Quantified Horn Clauses |
| 11.00 - 11.30 | Danilo Vendraminetto (Politecnico di Torino) Optimization Techniques for Craig Interpolant Compaction in Unbounded Model Checking |
| 11.30 - 12.00 | Marco Palena (Politecnico di Torino) Trading-off incrementality and dynamic restart of multiple solvers in IC3 |
| Lunch | |
| Session 4 | |
| 14.00 - 14.30 | Thomas Ferrére (Verimag) Efficient Robust Monitoring of STL |
| 14.30 - 15.00 | Dario Socci (Verimag) Mixed Critical Earliest Deadline First |
| 15.00 - 15.30 | Sergio Mover (FBK) Time-Aware Relational Abstractions for Hybrid Systems |
| Break | |
| Session 5 | |
| 16.00 - 16.30 | Florian Leitner-Fischer (Univ. of Konstanz) Recent Advances in Causality Checking Slides |
| 16.30 - 17.00 | Cristian Mattarei (FBK) Automated Analysis of Reliability Architecture Slides |
| Alpine Social Event | |
Wednesday (May 29th)
| Session 6 | |
| 09.00 - 09.30 | Ioan Dragan (TU Wien) Solving systems of linear inequalities using Bound Propagation in Vampire |
| 09.30 - 10.00 | Bas Schaafsma (Univ. of Trento / FBK) Pluggable SAT-Solvers for SMT-Solvers Slides |
| Break | |
| Session 7 | |
| 10.30 - 11.00 | Peter Lammich (TU Munich) Dynamic Pushdown Networks with Join and Contextual Locking |
| 11.00 - 11.30 | Peter Haring (Univ. of Passau) Distributing verification tasks with VerifierCloud |
| 11.30 - 12.00 | Carmelo Loiacono (Politecnico di Torino) New trends in Fast Cone-Of-Influence Computation and Usage in Problems with Multiple Properties |