| March 30, 2011 | |||
| Wednesday | |||
| 9:00-10:00 in E2.2 Invited Talk: Gerard J. Holzmann | |||
| 10:00-10:30 Coffee break | |||
| Wednesday 10:30-12:30 | |||
| TACAS | FASE | ESOP | FOSSACS |
| Games and Automata | Verification | Abstract Interpretation | Semantics |
| in E1.3/001 | in E2.1/001 | in E1.3/002 | in E1.3/003 |
| GAVS+: An Open Platform for the Research of Algorithmic Game Solving (Tool) | An interface theory for service-oriented design | Improving Strategies via SMT Solving | A Step-indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces |
| Chih-Hong Cheng, Alois Knoll, Christian Buckl, Michael Luttenberger | José Luiz Fiadeiro, Antónia Lopes | Thomas Martin Gawlitza, David Monniaux | Jan Schwinghammer, Lars Birkedal, Kristian Støvring |
| Büchi Store: An Open Repository of Büchi Automata (Tool) | rt-inconsistency: a new property for real time requirements | Transfer Function Synthesis without Quantifier Elimination | A Modified GoI Interpretation for a Linear Functional Programming Language and its Adequacy |
| Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, Yi-Wen Chang | Amalinda Post, Jochen Hoenicke, Andreas Podelski | Joerg Brauer, Andy King | Naohiko Hoshino |
| QUASY: Quantitative Synthesis Tool (Tool) | Automatic flow analysis for event-B | Generalizing the Template Polyhedral Domain | Estimation of the length of interactions in arena game semantics |
| Krishnendu Chatterjee, Thomas Henzinger, Barbara Jobstmann, Rohit Singh | Jens Bendisposto, Michael Leuschel | Michael Colon, Sriram Sankaranarayanan | Pierre Clairambault |
| Unbeast: Symbolic Bounded Synthesis (Tool) | Semantic quality attributes for big-step modeling languages | Linear Absolute Value Relation Analysis | Synchronous Game Semantics via Round Abstraction |
| Rüdiger Ehlers | Shahram Esmaeilsabzali, Nancy Day | Liqian Chen, Antoine Miné, Ji Wang, Patrick Cousot | Dan Ghica, Mohamed Nabih Menaa |
| 12:30-14:00 Lunch | |||
| 14:00-15:00 in E2.2 Invited Talk: Andrew Appel | |||
| Wednesday 15:15-16:15 | |||
| TACAS | FASE | FOSSACS - A | FOSSACS - B |
| Verification I | Specification and Modelling | Security | Binding |
| in E1.3/001 | in E2.1/001 | in E1.3/002 | in E1.3/003 |
| Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy | Formalizing and operationalizing industrial standards | Asymptotic information leakage under one-try attacks | Freshness and name-restriction in sets of traces with names |
| Sebastian Kupferschmid, Martin Wehrle | Dominik Dietrich, Lutz Schröder, Ewaryst Schulz | Michele Boreale, Francesca Pampaloni, Michela Paolini | Murdoch Gabbay, Vincenzo Ciancia |
| The ACL2 Sedan Theorem Proving System (Tool) | Modelling non-linear crowd dynamics in Bio-PEPA | A Trace-Based View on Operating Guidelines | Polymorphic Abstract Syntax via Grothendieck Construction |
| Harsh
Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios, Daron Vroon |
Mieke Massink, Diego Latella, Andrea Bracciali, Jane Hillston | Christian Stahl, Walter Vogler | Makoto Hamana |
| 16:15-16:45 Coffee break | |||
| Wednesday 16:45-18:15 | |||
| TACAS | FASE | ESOP | FOSSACS |
| Probabilistic Systems | Reachability and Model Checking | Language-based Security | Program Analysis |
| in E1.3/001 | in E2.1/001 | in E1.3/002 | in E1.3/003 |
| On Probabilistic Parallel Programs with Process Creation and Synchronisation | Smart reduction | Secure the Clones: Static Enforcement of Policies for Secure Object Copying | HTML Validation of Context-Free Languages |
| Stefan Kiefer, Dominik Wojtczak | Pepijn Crouzen, Frederic Lang | Thomas Jensen, Florent Kirchner, David Pichardie | Anders Møller, Mathias Schwarz |
| Confluence Reduction for Probabilistic Systems | Uniform Monte-Carlo model checking | Compiling Information-Flow Security to Minimal Trusted Computing Bases | On the Power of Cliques in Parameterized Verification of Ad Hoc Networks |
| Mark Timmer, Mariëlle Stoelinga, Jaco van de Pol | Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Richard Lassaigne, Sylvain Peyronnet | Cédric Fournet, Jérémy Planul | Giorgio Delzanno, Arnaud Sangnier, Gianluigi Zavattaro |
| Model Repair for Probabilistic Systems | Model checking Büchi push-down systems | From Exponential to Polynomial-time Security Typing via Principal Types | The reduced product of abstract domains and the combination of decision procedures |
| Ezio Bartocci, Radu Grosu, Panagiotis Katsaros, CR Ramakrishnan, Scott Smolka | Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin | Sebastian Hunt, David Sands | Patrick Cousot, Radhia Cousot, Laurent Mauborgne |
| 20:00: Banquet at Völklinger Hütte | |||