ETAPS 2015 Programme Monday - Friday

Monday 13 April

• Alexander Knapp, Till Mossakowski, Markus Roggenbach and Martin Glauer. An Institution for Simple UML State Machines
• Abel Gómez, Massimo Tisi, Gerson Sunyé and Jordi Cabot. Map-based Transparent Persistence for Very Large Models
• Emil Andriescu, Thierry Martinez and Valerie Issarny. Composing Message Translators and Inferring their Data Types using Tree Automata
• Christian Brenner, Joel Greenyer and Wilhelm Schäfer. On-the-fly Synthesis of Scarcely Synchronizing Distributed Controllers from Scenario-Based Specifications

• Konstantinos Mamouras. Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism
• Paul-André Melliès and Charles Grellois. An infinitary model of linear logic
• Pierre Clairambault and Peter Dybjer. Game Semantics and Normalization by Evaluation
• Martín Abadi, Frank McSherry and Gordon Plotkin. Foundations of Differential Dataflow

• Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki and André Platzer. A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
• Fabian Immler. Verified Reachability Analysis of Continuous Systems
• Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta. HYCOMP - an SMT-based model checker for hybrid systems
• Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan and Matthew Potok. C2E2: A Verification Tool For Annotated Stateflow Models

• Seema Jehan, Ingo Pill and Franz Wotawa. BPEL Integration Testing
• Johannes Bürdek, Malte Lochau, Stefan Bauregger, Andreas Holzer, Alexander von Rhein, Sven Apel and Dirk Beyer. Facilitating Reuse in Multi-Goal Test-Suite Generation for Software Product Lines
• Mike Czech, Marie-Christine Jakobs and Heike Wehrheim. Just test what you cannot verify!
• David Landsberg, Hana Chockler, Daniel Kroening and Matt Lewis. Evaluation of measures for Statistical Fault Localisation and an Optimising Scheme

• Bart Jacobs, Bas Westerbaan and Bram Westerbaan. States of Convex Sets
• Matthijs Vákár. Syntax and Semantics of Linear Dependent Types
• Joost Winter. A completeness result for finite lambda-bisimulations
• Ranald Clouston and Rajeev Goré. Sequent Calculus in the Topos of Trees

• Elvira Albert, Jesús Correas Fernández and Guillermo Román-Díez. Non-Cumulative Resource Analysis
• Shrawan Kumar, Amitabha Sanyal and Uday Khedker. Value Slice: A New Slicing Concept for Scalable Property Checking
• Reng Zeng, Zhuo Sun, Su Liu and Xudong He. A Method for Improving the Precision and Coverage of Atomicity Violation Predictions
• Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha and Bow-Yaw Wang. Commutativity of Reducers

• Rick Salay and Marsha Chechik. A Generalized Formal Framework for Partial Modeling
• Davide Arcelli, Vittorio Cortellessa and Catia Trubiani. Performance-based Software Model Refactoring in Fuzzy Contexts
• Kristopher Born, Thorsten Arendt, Florian Heß and Gabriele Taentzer. Analyzing Conflicts and Dependencies of Rule-Based Transformations in Henshin (short talk)

• Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics
• Laura Bozzelli, Bastien Maubert and Sophie Pinchinat. Unifying Hyper Logic and Epistemic Temporal Logic

• Hiroshi Unno and Tachio Terauchi. Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling
• Kedar Namjoshi and Richard Trefler. Analysis of Dynamic Process Networks

Tuesday 14 April

• Andrew D. Gordon, Claudio Russo, Marcin Szymczak, Johannes Borgstrom, Nicolas Rolland, Thore Graepel and Daniel Tarlow. Probabilistic Programs as Spreadsheet Queries
• Tie Cheng and Xavier Rival. Static Analysis of Spreadsheet Applications for Type-Unsafe Operations Detection
• Neil Toronto, Jay McCarthy and David Van Horn. Running Probabilistic Programs Backwards
• Manuel Eberl, Johannes Hölzl and Tobias Nipkow. A Verified Compiler for Probability Density Functions

• Van Chan Ngo, Jean-Pierre Talpin and Thierry Gautier. Translation Validation for Clock Transformations in a Synchronous Compiler
• Grigory Fedyukovich, Andrea Callia D'Iddio, Antti Hyvärinen and Natasha Sharygina. Symbolic Detection of Assertion Dependencies for Bounded Model Checking
• Stefan Blom, Saeed Darabi and Marieke Huisman. Verification of Loop Parallelisations
• Manuel Clavel and Carolina Dania. Model-based formal reasoning about data-management applications

• Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen and Radu Mardare. On the Total Variation Distance of Semi-Markov Chains
• Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan and Yue Ben. Decidable and Expressive classes of Probabilistic Automata
• Blaise Genest, Doron Peled and Sven Schewe. Knowledge = observation + memory + computation
• Daniel Gebler, Kim Guldstrand Larsen and Simone Tini. Compositional metric reasoning with Probabilistic Process Calculi

• Pavol Cerny, Thomas A. Henzinger, Laura Kovacs, Arjun Radhakrishna and Jakob Zwirchmayr. Segment Abstraction for Worst-Case Execution Time Analysis
• Jan Hoffmann and Zhong Shao. Automatic Static Cost Analysis for Parallel Programs
• Willem Penninckx, Bart Jacobs and Frank Piessens. Sound, modular and compositional verification of the input/output behavior of programs
• Cristina David, Daniel Kroening and Matt Lewis. Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs

• Radu Calinescu, Simos Gerasimou and Alec Banks. Self-Adaptive Software with Decentralised Control Loops
• Carlos Canal and Gwen Salaün. Model-Based Adaptation of Software Communicating via FIFO Buffers
• Ahmed Bouajjani, Georgel Calin, Egor Derevenetc and Roland Meyer. Lazy TSO Reachability
• Daniel Strüber, Julia Rubin, Marsha Chechik and Gabriele Taentzer. A Variability-Based Approach to Reusable and Efficient Model Transformations

• Tomas Brazdil, Krishnendu Chatterjee, Vojtech Forejt and Antonin Kucera. MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives
• Ramiro Demasi, Nicolas Ricci, Pablo Castro, Tom Maibaum and Nazareno Aguirre. syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications
• Nikolaj Bjorner, Anh-Dung Phan and Lars Fleckenstein. νZ - An Optimizing SMT Solver
• Soonho Kong, Sicun Gao, Wei Chen and Edmund Clarke. dReach: Delta-Reachability Analysis for Hybrid Systems
• Alexandre David, Peter G. Jensen, Kim G. Larsen, Marius Mikucionis and Jakob H. Taankvist. STRATEGO: Verification, Performance Analysis and Optimization of Timed Game Strategies
• Adel Djoudi and Sébastien Bardin. BINSEC: Binary-level analysis with Low-Level Regions
• Emmanuel Fleury, Olivier Ly, Gérald Point and Aymeric Vincent. Insight: An Open Binary Analysis Framework
• Gabriele Costa, Alessandro Armando, Alessio Merlo, Gabriele De Maglie, Gianluca Bocci, Giantonio Chiarelli and Rocco Mammoliti. SAM: the Static Analysis Module of the MAVERIC Mobile App Security Verification Platform
• Yann Thierry-Mieg. Symbolic model-checking using ITS-Tools

• Pierre Neron, Andrew Tolmach, Eelco Visser and Guido Wachsmuth. A Theory of Name Resolution
• Giuseppe Castagna, Hyeonseung Im, Kim Nguyễn and Véronique Benzaken. A Core Calculus for XQuery 3.0: Combining Navigational and Pattern Matching Approaches
• Ravi Chugh. IsoLate: A Type System for Self-Recursion

• Conrad Cotton-Barratt, David Hopkins, Andrzej Murawski and Luke Ong. Fragments of ML Decidable by Nested Data Class Memory Automata
• Guilhem Jaber. Operational Nominal Game Semantics
• Aleš Bizjak and Lars Birkedal. Step-Indexed Logical Relations for Probability

TACAS tool demo market (Chair: Jaco van de Pol) / Room: Octagon

Start at 16:45

Wednesday 15 April

Room: Great Hall
Invited Talk: Wang Yi (Uppsala University, Sweden)

Scalable Timing Analysis with Refinement
(Nan Guan, Yue Tang, Jakaria Abdullah, Martin Stigge, and Wang Yi)

Abstract: Traditional timing analysis techniques rely on composing system-level worst-case behavior with local worst-case behaviors of individual components. In many complex real-time systems, no single local worst-case behavior exists for each component and it generally requires to enumerate all the combinations of individual local behaviors to find the global worst case. This paper presents a scalable timing analysis technique based on abstraction refinement, which provides effective guidance to significantly prune away state space and quickly verify the desired timing properties. We first establish the general framework of the method, and then apply it to solve the analysis problem for several different real-time task models

Chair: Christel Baier

• Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod and Peter Sewell. The Problem of Programming Language Concurrency Semantics
• Parosh Aziz Abdulla, Mohamed Faouzi Atig and Tuan Phong Ngo. The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO
• Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
• Jasmin Chrstian Blanchette, Andrei Popescu and Dmitriy Traytel. Witnessing (Co)datatypes

• Stefan Kiefer, Ines Marusic and James Worrell. Minimisation of Multiplicity Tree Automata
• Yaron Velner. Robust Multidimensional Mean-Payoff Games are Undecidable
• Hsi-Ming Ho and Joel Ouaknine. The Cyclic-Routing UAV Problem is PSPACE-complete
• Sylvain Salvati and Igor Walukiewicz. Typing weak MSOL properties

• by Jeffery Hansen, Lutz Wrage, Sagar Chaki, Dionisio De Niz and Mark Klein. Semantic Importance Sampling for Statistical Model Checking
• Parosh Nicolas Basset, Marta Kwiatkowska, Ufuk Topcu and Clemens Wiltsche. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives
• Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts and Alessandro Abate. FAUST2: Formal Abstractions of Uncountable-STate STochastic processes

• Burke Fetscher, Koen Claessen, Michał Pałka, John Hughes and Robby Findler. Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System
• Ezgi Çiçek, Deepak Garg and Umut Acar, Refinement Types for Incremental Computational Complexity
• Jeremy Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt and Ronald Garcia. Monotonic References for Efficient Gradual Typing
• Stefan Schulze Frielinghaus, Michael Petter and Helmut Seidl. Inter-procedural Two-Variable Herbrand Equalities

• Nuno Macedo, Alcino Cunha and Tiago Guimarães. Exploring Scenario Exploration
• Kenan Liu, Gustavo Pinto and Yu David Liu. Data-Oriented Characterization of Application-Level Energy Optimization
• Seung Yeob Shin, Yuriy Brun, Leon Osterweil, Hari Balasubramanian and Philip L. Henneman. Resource Specification for Prototyping Human-Intensive Systems
• Martín Abadi. The Prophecy of Undo

• Jeroen Bransen, L. Thomas van Binsbergen, Koen Claessen and Atze Dijkstra. Linearly Ordered Attribute Grammar scheduling using SAT-solving
• Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia and Moshe Y. Vardi. On Parallel Scalable Uniform SAT Witness Generation
• Dmitry Chistikov, Rayna Dimitrova and Rupak Majumdar. Approximate Counting in SMT and Value Estimation for Probabilistic Programs
• Roberto Sebastiani and Patrick Trentin. Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions

• Arlen Cox, Bor-Yuh Evan Chang and Xavier Rival. Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages
• Stefano Calzavara, Michele Bugliesi, Silvia Crafa and Enrico Steffinlongo. Fine-grained Detection of Privilege Escalation Attacks on Browser Extensions
• Michael Emmi, Pierre Ganty, Rupak Majumdar and Fernando Rosa-Velardo. Analysis of Asynchronous Programs with Event-Based Synchronization

• Timos Antonopoulos, Paul Hunter, Shahab Raza and James Worrell. Three Variables Suffice for Real-Time Logic
• Peter Habermehl and Dietrich Kuske. On Presburger arithmetic extended with modulo counting quantifiers
• Moses Ganardi. Parity Games of Bounded Tree- and Clique-Width

• Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson and Konstantinos Sagonas. Stateless Model Checking for TSO and PSO
• Anton Wijs. GPU Accelerated Strong and Branching Bisimulation Checking
• Byron Cook, Heidy Khlaaf and Nir Piterman. Fairness for Infinite-State Systems

Thursday 16 April

Room: Great Hall
Invited Talk: Catuscia Palamidessi (INRIA Saclay and LIX, France)

Extended Differential Privacy and Applications to Location Privacy

Abstract: In this talk, we review the notion of Differential Privacy,  its implications in terms of Bayesian Adversary, and we discuss typical implementations from the point of view of their optimality with respect to utility. Then, we consider an extension of differential privacy to general metric domains, and the consequences for the optimality results. Finally, we show an instantiation to the case of location privacy, leading to the notion of geo-indistinguishability. We conclude by illustrating some research direction that may be interesting for the ETAPS community.

Chair: Riccardo Focardi

• Sam Lindley and J. Garrett Morris. A Semantics for Propositions as Sessions
• Alexey Gotsman and Hongseok Yang. Composite Replicated Data Types
• Tachio Terauchi and Hiroshi Unno. Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement
• Aws Albarghouthi, Josh Berdine, Byron Cook and Zachary Kincaid. Spatial Interpolants

• Stefan Heule, Deian Stefan, Edward Yang, John Mitchell and Alejandro Russo. IFC Inside: Retrofitting Languages with Dynamic Information Flow Control
• Bart van Delft, Sebastian Hunt and David Sands. Very Static Enforcement of Dynamic Policies
• Adam Petcher and Greg Morrisett. The Foundational Cryptography Framework
• Martín Abadi and Michael Isard. On the Flow of Data, Information, and Time

• Dirk Beyer. Software Verification and Verifiable Witnesses (Report on SV-COMP 2015)
• Thomas Stroeder, Cornelius Aschermann, Florian Frohn, Jera Hensel and Jürgen Giesl. AProVE: Termination and Memory Safety of C Programs
• Dexi Wang, Chao Zhang, Guang Chen, You Peng, Fei He, Ming Gu and Jiaguang Sun. Beagle: Model Checking of C Programs Using LLVM
• Vadim Mutilin, Mikhail Mandrykin and Pavel Shved. Predicate Analysis with BLAST 2.7.3
• Wei Wang and Clark Barrett. Cascade
• Daniel Kroening and Michael Tautschnig. CBMC - C Bounded Model Checker
• Matthias Dangl, Stefan Löwe and Philipp Wendler. CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic
• Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang and Farn Wang. CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation
• Pablo Gonzalez-de-Aledo and Pablo Sanchez. FramewORk for Embedded System verificaTion
• Lukas Holik, Martin Hruska, Ondrej Lengal, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar. Forester: Shape Analysis Using Tree Automata
• Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre and Gennaro Parlato. Lazy-CSeq 0.6c: An Improved Lazy Sequentialization Tool for C
• Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre and Gennaro Parlato. MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings
• Franck Cassez, Takashi Matsuoka, Edward Pierzchalski and Nathan Smyth. Perentie: Modular Trace Refinement and Selective Value Tracking
• Petr Muller, Petr Peringer and Tomas Vojnar. Predator Hunting Party
• Arie Gurfinkel, Temesghen Kahsai and Jorge A Navas. SeaHorn: A Framework for Verifying C Programs
• Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer and Zvonimir Rakamaric. SMACK+Corral: A Modular Verifier
• Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa and Andreas Podelski. Ultimate Automizer with Array Interpolation
• Alexander Nutz, Daniel Dietsch, Mostafa Mahmoud Mohamed and Andreas Podelski. Ultimate Kojak with Memory Safety Checks
• Truc L. Nguyen, Bernd Fischer, Salvatore La Torre and Gennaro Parlato. Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches

• Cristina David, Daniel Kroening and Matt Lewis. Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs
• Gabriel Scherer and Didier Rémy. Full reduction in the face of absurdity
• Azalea Raad, Jules Villard and Philippa Gardner. CoLoSL: Concurrent Local Subjective Logic
• Filip Sieczkowski, Kasper Svendsen, Lars Birkedal and Jean Pichon-Pharabod. A Separation Logic for Fictional Sequential Consistency

• Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl and Lars Birkedal. Programming and Reasoning with Guarded Recursion for Coinductive Types
• Daniel Leivant and Ramyaa Ramyaa. The computational contents of ramified corecurrence
• Amina Doumane, Alexis Saurin and Marc Bagnol. On the dependencies of logical rules
• Aleksy Schubert, Pawel Urzyczyn and Konrad Zdanowski. On the Mints Hierarchy in First-Order Intuitionistic Logic

• Zaruhi Aslanyan and Flemming Nielson. Pareto Efficient Solutions of Attack-Defence Trees
• Fatih Turkmen, Jerry den Hartog, Silvio Ranise and Nicola Zannone. Analysis of XACML Policies with SMT

• Mirco Giacobbe, Calin Guet, Ashutosh Gupta, Thomas Henzinger, Tiago Paixao and Tatjana Petrov. Model checking gene regulatory networks
• Ocan Sankur. Symbolic Quantitative Robustness Analysis of Timed Automata

• Wilmer Ricciotti. Binding Structures as an Abstract Data Type
• Pedro Vasconcelos, Steffen Jost, Mario Florido and Kevin Hammond. Type-based Allocation Analysis for Co-Recursion in Lazy Functional Languages
• Eric Seidel, Niki Vazou and Ranjit Jhala. Type Targeted Testing

Tutorial / Room: PP1

Daniel J. Bernstein (University of Illinois at Chicago, USA & Technische Universiteit Eindhoven, Netherlands). The death of optimizing compilers

This tutorial is an introduction to (1) what current and near-future processors are capable of; (2) how modern high-speed software libraries actually work; and (3) the increasing dominance of domain-specific tools to engineer high-speed software. This tutorial is designed to be fully comprehensible to audience members who are not optimization experts.

• Rajeev Alur, Salar Moarref and Ufuk Topcu. Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
• Roderick Bloem, Krishnendu Chatterjee, Swen Jacobs and Robert Koenighofer. Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
• Roderick Bloem, Bettina Konighofer, Robert Konighofer and Chao Wang. Shield Synthesis: Runtime Enforcement for Reactive Systems

Friday 17 April

Room: Great Hall
Invited Talk: Keshav Pingali (University of Texas, USA)

A Graphical Model for Context-Free Grammar Parsing

(Keshav Pingali and Gianfranco Bilardi )

Abstract: In the compiler literature, parsing algorithms for context-free grammars are presented using string rewriting systems or abstract machines such as pushdown automata. Unfortunately, the resulting descriptions can be baroque, and even a basic understanding of some parsing algorithms, such as Earley’s algorithm for general context-free grammars, can be elusive. In this paper, we present a graphical representation of context-free grammars called the Grammar Flow Graph (GFG) that permits parsing problems to be phrased as path problems
in graphs; intuitively, the GFG plays the same role for context-free grammars that nondeterministic finite-state automata play for regular grammars. We show that the GFG permits an elementary treatment of Earley’s algorithm that is much easier to understand than previous descriptions of this algorithm. In addition, look-ahead computation can be expressed as a simple inter-procedural dataflow analysis problem, providing an unexpected link between front-end and back-end technologies in compilers. These results suggest that the GFG can be a new foundation for the study of context-free grammars

Chair: Björn Franke

• Amanj Sherwany, Nate Nystrom and Nosheen Zaza. A refactoring library for Scala compiler extensions
• Vincent St-Amour, Leif Andersen and Matthias Felleisen. Feature-Specific Profiling
• Timothy Bourke, Jean-Louis Colaco, Cédric Pasteur, Bruno Pagano and Marc Pouzet. A Synchronous-based Code Generator For Explicit Hybrid Systems Languages
• Ali Afroozeh and Anastasia Izmaylova. Faster, Practical GLL Parsing

• Tom Chothia, Ben Smyth and Christopher Staite. Automatically Checking Commitment Protocols in ProVerif Without False Attacks
• Sjouke Mauw and Sasa Radomirovic. Generalizing Multi-Party Contract Signing
• Sibylle Froeschle. Leakiness is Decidable for Well-Founded Protocols
• Thanh Binh Nguyen and Christoph Sprenger. Abstractions for Security Protocol Verification

• Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre and Gennaro Parlato. Verifying Concurrent Programs by Memory Unwinding
• Julian Tschannen, Carlo A. Furia, Martin Nordio and Nadia Polikarpova. AutoProof: Auto-active Functional Verification of Object-oriented Programs
• Adrian Francalanza and Clare Cini. An LTL Proof System for Runtime Verification
• Giles Reger, Helena Cuenca Cruz and David Rydeheard. MarQ: Monitoring At Runtime with QEA

• Hilmar Ackermann, Christoph Reichenbach, Yannis Smaragdakis and Christian Müller. A Backend Extension Mechanism for PQL/Java with Free Run-Time Optimisation
• Nicholas Allen, Bernhard Scholz and Paddy Krishnan. Staged Points-To Analysis for Large Code Bases
• Alain Darte and Alexandre Isoard. Exact and Approximated Data-Reuse Optimizations for Tiling with Parametric Sizes
• Sebastian Buchwald. Optgen: A Generator for Local Optimizations

• Robert Künnemann. Automated Backward Analysis of PKCS#11 v2.20
• Kristian Beilke and Volker Roth. A Safe Update Mechanism for Smart Cards
• Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott. Discrete vs Dense Times in the Verification of Cyber-Physical Security Protocols
• Vincent Cheval and Veronique Cortier. Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques

• Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon and Denis Poitrenaud. Parallel Explicit Model Checking for Generalized Büchi Automata
• Dileep Kini and Mahesh Viswanathan. Probabilistic Büchi Automata for LTL\GU
• Vince Molnár, Dániel Darvas, András Vörös and Tamás Bartha. Saturation-based Incremental LTL Model Checking with Inductive Proofs
• Tomas Fiedor, Lukas Holik, Ondrej Lengal and Tomas Vojnar. Nested Antichains for WS1S

• Nicholas Hollingum and Bernhard Scholz. Towards a Scalable Framework for Context-free Language Reachability
• Nicholas Ng, Jose Gabriel de Figueiredo Coutinho and Nobuko Yoshida. Protocols by Default: Safe MPI Code Generation based on Session Types.
• Delphine Demange, David Pichardie and Léo Stéfanesco. Verifying Fast and Sparse SSA-based Optimizations in Coq

• Veronique Cortier, Fabienne Eigner, Steve Kremer, Matteo Maffei and Cyrille Wiedling. Type-Based Verification of Electronic Voting Protocols
• Myrto Arapinis, Vincent Cheval and Stephanie Delaune. Composing Security Protocols: from Confidentiality to Privacy
• Michael Backes, Fabian Bendun, Jörg Hoffmann and Ninja Marnau. PriCL: Creating a Precedent, a Framework for Reasoning About Privacy Case Law

• Tom van Dijk and Jaco van de Pol. Sylvan: Multi-core Decision Diagrams
• Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom and Tom van Dijk. LTSmin: High-Performance Language-Independent Model Checking
• Abderahman Kriouile and Wendelin Serwe. Using a Formal Model to Improve Verification of a Cache Coherent System-on-Chip