Workshop Program

Saturday, June 30

9:00 – 10:00: Invited Talk (joint with COMPARE'12)

10:00 – 10:30: Coffee Break

10:30 – 12:00: Session I: Logics, Proofs, and Strategies

A. Zeljic, Ph. Rümmer:
Experiments with Automated Strategy Selection in a Theorem Prover
M. P. Bonacina and N. Dershowitz
Abstract Canonical Inference: On Fairness in Theorem Proving
M. Nikolic, P. Janicic:
CDCL-Based Abstract State Transition System for Coherent Logic

12:00 – 13:30: Lunch

13:30 – 15:00: Session II: Analysis of Software & Hybrid Systems

C. Colombo, G. Pace:
Monitoring-Oriented Compensation Programming
D. Monniaux, J. Henry, M. Moy, L. Gonnord:
Path-focused analysis of numerical transitions
P. Jackson:
Better Real Arithmetic Provers for Hybrid Systems Verification

15:00 – 15:30: Coffee Break

in parallel:

15:30 – 16:30: COST-Action "Rich-Model Toolkit" Management Committee Meeting

15:30 – 17:00: Open Problems Session (Part I)

9:00 – 10:00: Invited Talk (joint with IWS'12)

10:00 – 10:30: Coffee Break

10:30 – 12:00: Session III: Security & Certificates

B. Beckert, D. Bruns, V. Klebanov, P.H. Schmitt, C. Scheben, M. Ulbrich:
Secure Information Flow for Java: A Dynamic Logic Approach
S. Ratschan:
Certificates for Reachability and Progress of Discrete and Continuous Systems
A. Niemetz, M. Preiner, F. Lonsing, M. Seidl and A. Biere:
Scalable Certificate Extraction for QBF

12:00 – 13:30: Lunch

13:30 – 15:00: Session IV: Model Checking

S. Wieringa:
Reviewing the Results of the Hardware Model Checking Competition 2011
M. Seidl:
Model Checking UML Models: State-of-the-Art and Challenges
S. Falke, F. Merz, C. Sinz:
Simplification Techniques in Software Bounded Model Checking

15:00 – 15:30: Coffee Break

15:30 – 16:30: Session V: Applications

E. Jahren:
SAT-based Techniques for the Car Sequencing Problem
A. Bauer, P. Baumgartner, M. Norrish:
Reasoning with Data-Centric Business Processes

16:30 – 16:45: Interval

16:45 – 17:30: Open Problems Session (Part II)