| 9:00
| Opening
| Francesco Logozzo and Lenore Zuck
|
| 9:10
| Invited Talk: Abstract Interpretation of Non-monotone Bi-inductive Semantic Definitions
| Radhia Cousot
|
| 10:10
| break
|
|
|
| Abstract Interpretation I Accepted papers. Chair: TBA
|
|
| 10:30
| Model checking for action abstraction
| Harald Fecher and Michael Huth
|
| 11:00
| Abstract Interpretation of the Physical Inputs of Embedded Programs
| Olivier Bouissou and Matthieu Marte
|
| 11:30
| A Forward-Backward Abstraction Refinement Algorithm
| Francesco Ranzato, Olivia Rossi Doria and Francesco Tapparo
|
| 12:00
| Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?
| Rayna Dimitrova and Andreas Podelski
|
| 12:30
| Lunch
|
|
| 14:00
| Invited Tutorial: Verification of Register Allocation
| Jens Palsberg
|
| 16:00
| Break
|
|
|
| Abstract Interpretation II Accepted papers. Chair: TBA
|
|
| 16:30
| Deriving Bisimulations by Simplifying Partitions
| Isabella Mastroeni
|
| 17:00
| Abstract interpretation of cellular signalling networks
| Vincent Danos, Jerome Feret, Walter Fontana and Jean Krivine.
|
| 17:30
| An Improved Tight Closure Algorithm for Integer Octagonal Constraints
| Roberto Bagnara, Patricia Hill and Enea Zaffanella
|
| 9:00
| Invited Talk:CTL as an intermediate language
| Neil Jones
|
|
| Accepted papers. Chair: Agostino Cortesi
|
|
| 9:45
| All You Need is Compassion
| Amir Pnueli and Yaniv Sa'ar
|
| 10:15
| break
|
|
| 10:45
| From LTL to Symbolically Represented Deterministic Automata
| Klaus Schneider and Andreas Morgenstern
|
| 11:15
| Monitoring Temporal Properties of Stochastic Systems
| A. Prasad Sistla and Abhigna Srinivas
|
| 11:45
| Approximation Refinement for Interpolation Based Model Checking
| Vijay D'silva, Mitra Purandare and Daniel Kroening.
|
| 12:15
| Extending Model Checking with Dynamic Analysis
| Alex Groce and Rajeev Joshi
|
| 12:45
| Lunch
|
|
| 14:00
| Invited Tutorial: Program analysis and programming languages for security
| Marco Pistoia
|
| 16:00
| Break
|
|
|
| Accepted papers. Chair: TBA
|
|
| 16:30
| Precise Set Sharing Analysis for Java-style Programs
| Mario Mendez-Lojo and Manuel Hermenegildo
|
| 17:00
| Internal and External Logics of Abstract Interpretations
| David Schmidt
|
| 17:30
| A Hybrid Algorithm for LTL Games
| Saqib sohail, Fabio Somenzi and Kavita Ravi
|
| 19:30
| Special Evening Workshop Joint with 30YAI
| Details
|
| 9:00
| Invited Talk:Taking Concurrency Seriously: the Multicore Challenge
| Maurice Herlihy
|
| 10:00
| break
|
|
|
| Accepted papers. Chair: Maurice Herlihy
|
|
| 10:20
| Sufficient Preconditions for Modular Assertion Checking
| Yannick Moy
|
| 10:50
| Handling Parameterized Systems with Non-Atomic Global Conditions
| Noomene Ben Henda, Ahmed Rezine, Parosh Abdulla and Giorgio Delzanno
|
| 11:20
| On Bridging Simulation and Formal Verification
| Eugene Goldberg
|
| 11:50
| Decision Procedures for Multisets with Cardinality Constraints
| Ruzica Piskac and Viktor Kuncak
|
| 12:20
| Lunch
|
|
| 13:40
| Invited Tutorial: Multivalued Logics, automata, simulations and games
| Orna Kupferman
|
| 15:10
| Break
|
|
|
| Accepted papers. Chair: Orna Kupferman
|
|
| 15:30
| Runtime Checking for Separation Logic
| Huu Hai Nguyen, Viktor Kuncak and Wei Ngan Chin
|
| 16:00
| Diagnostic Informat ion for Realizability
| Alessandro Cimatti, Marco Roveri, Viktor Schuppan and Andrei Tchaltsev
|
| 16:30
| Break
|
|
| 16:40
| 30YAI
| Patrick Cousot
|