Best Paper Awards

EATCS Best Paper Award

• Pablo Barenbaum and Eduardo Bonelli. Sharing and Linear Logic with Restricted Access (FoSSaCS)
• Patricia Bouyer, B Srivathsan and Vaishnavi Vishwanath. Model-checking real-time systems: revisiting the alternating automaton route (FASE)

EASST Best Paper Award

• Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofroň, and Natasha Sharygina. Unsatisfiability Proofs for Horn Solving (TACAS)

EAPLS Best Paper Award

• Sung-Shik Jongmans. First-Person Choreographic Programming with Continuation-Passing Communications (ESOP)

Best Tool Paper Award

• Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym, and Jan Midtgaard. Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM (TACAS)

Distinguished Paper Awards

• Jia Chen, Xiao Lei Chen, Jie Shi, Peng Wang, and Wei Wang. Voce: A Virtual on-Call Engineer For Automated Alert Incident Analysis Using A large Language Model

• Raffi Khatchadourian, Tatiana Castro Vélez, Mehdi Bagherzadeh, Nan Jia, and Anita Raja. Hybridize functions: A Tool For Automatically Refactoring Imperative Deep Learning Programs to Graph Execution

• Linan Chen, Florence Clerc, and Prakash Panangaden. A Behavioural Pseudometric For Continuous-time Markov Processes

• Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger and Patrick Wienhöft. Sound Statistical Model Checking For Probabilities and Expected Rewards

• Jan Kretinsky, Tobias Meggendorfer, Maximilian Prokop and Ashkan Zarkhah. SemML: Enhancing Automata-Theoretic Ltl Synthesis with Machine Learning

• Mohsen Ghaffari, Mahsa Varshosaz, Einar Broch Johnsen, and Andrzej Wasowski. Symbolic State Partitioning for Reinforcement Learning

• Liron Cohen, Reuben Rowe, and Matan Shaked. Cyclone: A Heterogeneous Tool For verifying Infinite Descent

• Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofroň, and Natasha Sharygina. Unsatisfiability Proofs for Horn Solving

• Risa Yamada, Naoki Kobayashi, Ken Sakayori, and Ryosuke Sato. On the Relationship Between Dijkstra Monads And Higher-order Fixpoint Logic

• Patricia Bouyer, B Srivathsan, and Vaishnavi Vishwanath. Model-checking Real-Time Systems: Revisiting the Alternating Automaton Route

• Sung-Shik Jongmans. First-Person Choreographic Programming with Continuation-Passing Communications

• Pablo Barenbaum and Eduardo Bonelli. Sharing and Linear Logic with Restricted Access

• Yoav Feisntein, Orna Kupferman, and Noam Shenwald. Non-Zero-Sum Games With Multiple Weighted Objectives

• Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym, and Jan Midtgaard. Dynamic Verification Of OCaml Software With Gospel And Ortac/QCheck-Stm

EATCS Best Paper Award

• Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas, Fredrik Tåquist. Scalable Tree-based Register Automata Learning (TACAS)

EASST Best Paper Award

• Nils Husung, Clemens Dubslaff, Holger Hermanns, and Maximilian Alexander Köhl. OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust (TACAS)

EAPLS Best Paper Award

• Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains

Best Tool Paper Award

• Raphaël Monat, Aymeric Fromherz, and Denis Merigoux. Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

Award Nominations

• Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč. Z3-Noodler: An Automata-based String Solver
• He Xu, Sven Schneider, and Holger Giese. Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems
• Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang, and Guojun Ma. Smart Issue Detection for Large-Scale Online Service Systems Using Multi-Channel Data
• Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni. Monadic Intersection Types, Relationally
• Paul Fiterau-Brostean, Simon Dierl, Falk Howar, Bengt Jonsson, Konstantinos Sagonas and Fredrik Tåquist. Scalable Tree-based Register Automata Learning
• Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
• Hrutvik Kanabar, Kacper Korban and Magnus O. Myreen. Verified Inlining and Specialisation for PureCake
• Balder ten Cate and Jesse Comer. Craig Interpolation for Decidable First-Order Fragments
• Nils Husung, Clemens Dubslaff, Holger Hermanns and Maximilian Alexander Köhl. OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust
• Raphaël Monat, Aymeric Fromherz and Denis Merigoux. Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
• Pierre Lermusiaux and Benoit Montagu. Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation

EATCS Best Paper Award

• Pascal Baumann, Flavio D’Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze and Georg Zetzsche. Unboundedness problems for machines with reversal-bounded counters (FoSSaCS)

EASST Best Paper Award

• Pantazis Deligiannis, Aditya Senthilnathan, Fahad Nayyar, Chris Lovett and Akash Lal. Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote (TACAS)

EAPLS Best Paper Award

• Daniel Lundén, Gizem Çaylak, Fredrik Ronquist and David Broman. Automatic Alignment in Higher-Order Probabilistic Programming Languages

SCP Best Tool Paper Award

• Raven Beutner and Bernd Finkbeiner. AutoHyper: Explicit-State Model Checking for HyperLTL

Award Nominations

• Daniel Lundén, Gizem Çaylak, Fredrik Ronquist and David Broman. Automatic Alignment in Higher-Order Probabilistic Programming Languages
• Yuito Murase, Yuichi Nishiwaki and Atsushi Igarashi. Contextual Modal Type Theory with Polymorphic Contexts
• Paulo Emílio de Vilhena and François Pottier. A Type System for Effect Handlers and Dynamic Labels
• Bernardo Subercaseaux and Marijn Heule. The Packing Chromatic Number of the Infinite Square Grid is 15
• Dawn Michaelson, Dominik Schreiber, Marijn Heule, Benjamin Kiesl-Reiter and Mike Whalen. Unsatisfiability Proofs for Distributed SAT Solvers
• Pantazis Deligiannis, Aditya Senthilnathan, Fahad Nayyar, Chris Lovett and Akash Lal. Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote
• Raven Beutner and Bernd Finkbeiner. AbaHyper: Sound and Complete Model Checking for HyperLTL
• Ramana Nagasamudram, Anindya Banerjee and David A. Naumann. The WhyRel Prototype for Relational Verification of Pointer Programs
• Arnd Hartmanns, Sebastian Junges, Tim Quatmann and Maximilian Weininger. A Practitioner’s Guide to MDP Model Checking Algorithms
• Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni and Roopsha Samanta. Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification
• Luiz Carvalho, Renzo Degiovanni, Matías Brizzio, Maxime Cordy, Nazareno Aguirre, Yves Le Traon and Mike Papadakis. ACoRe: Automated Goal-Conflict Resolution
• Sinem Getir Yaman, Charlie Burholt, Maddie Jones, Radu Calinescu and Ana Cavalcanti. Specification and Validation of Normative Rules for Autonomous Agents
• Pascal Baumann, Flavio D’Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze and Georg Zetzsche. Unboundedness problems for machines with reversal-bounded counters

EATCS Best Paper Award

• Emmanuel Hainry, Bruce Kapron, Jean-Yves Marion and Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime. FoSSaCS 2022

Award Nominations

• Christel Baier, Florian Funke, Jakob Piribauer and Robin Ziemek. On probability-raising causality in Markov decision processes. FoSSaCS 2022
• Geoff Cruttwell, Bruno Gavranovic, Neil Ghani, Paul Wilson, Fabio Zanasi. Categorical Foundation of Gradient-Based Learning. ESOP 2022
• Emmanuel Hainry, Bruce Kapron, Jean-Yves Marion and Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime. FoSSaCS 2022
• Sung-Shik Jongmans, Petra van den Bos. A Predicate Transformer for Choreographies. ESOP 2022

EASST Best Paper Award

• Ezio Bartocci, Thomas Ferrère, Thomas Henzinger, Dejan Nickovic and Ana Oliveira Da Costa. Information-flow Interface. FASE 2022

Award Nominations

• Georgiana Caltais, Hossein Hojjat, Mohammadreza Mousavi and Hünkar Can Tunç. DyNetKAT: An Algebra of Dynamic Network. FoSSaCS 2022
• Ezio Bartocci, Thomas Ferrère, Thomas Henzinger, Dejan Nickovic and Ana Oliveira Da Costa. Information-flow Interface. FASE 2022
• Luca Bortolussi, Giuseppe Maria Gallo, Jan Kretinsky and Laura Nenzi. Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes. TACAS 2022
• Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell. Relaxed virtual memory in Armv8-A. ESOP 2022
• Tamajit Banerjee, Majumdar Rupak, Mallik Kaushik, Anne-Kathrin Schmuck and Sadegh Soudjani. A Direct Symbolic Algorithm for Solving Stochastic Rabin Games. TACAS 2022

EAPLS Best Paper Award

• David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu and Emma Zhong. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. TACAS 2022

Award Nominations

• David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu and Emma Zhong. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. TACAS 2022
• Emmanuel Hainry, Bruce Kapron, Jean-Yves Marion and Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime. FoSSaCS 2022
• Sung-Shik Jongmans, Petra van den Bos. A Predicate Transformer for Choreographies. ESOP 2022

SCP Best Tool Paper Award

• Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS 2022

Award Nominations

• David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu and Emma Zhong. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. TACAS 2022
• Jorge Sousa Pinto, Cláudio Belo Lourenço. Why3-do: The Way of Harmonious Distributed System Proofs. ESOP 2022
• Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS 2022

EATCS Best Paper Award

• Robin Piedeleu and Fabio Zanasi. A String Diagrammatic Axiomatisation of Finite-State Automata. FoSSaCS 2021
• Bartek Klin, Sławomir Lasota and Szymon Toruńczyk. Nondeterministic and co-Nondeterministic Implies Deterministic, for Data Languages. FoSSaCS 2021

Award Nominations

• Randal E. Bryant and Marijn J. H. Heule. Generating Extended Resolution Proofs with a BDD-Based SAT Solver. TACAS 2021
• Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. Syntax-Guided Quantifier Instantiation. TACAS 2021
• Matthijs Vákár. Reverse AD at Higher Types: Pure, Principled and Denotationally Correct. ESOP 2021

EASST Best Paper Award

• Richard Schumi and Jun Sun. SpecTest: Specification-Based Compiler Testing. FASE 2021

Award Nominations

• Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian A. Kohl, Yannik Schnitzer and Maximilian Schwenger. RTLola on Board: Testing Real Driving Emissions on Your Phone. TACAS 2021
• Joshua Gleitze, Heiko Klare and Erik Burger. Finding a Universal Execution Strategy for Model Transformation Networks. FASE 2021
• Maximilian P. L. Haslbeck and Peter Lammich. For a Few Dollars More – Verified Fine-Grained Algorithm Analysis Down to LLVM. ESOP 2021

EAPLS Best Paper Award

• Rupak Majumdar, Ramanathan S. Thinniyam and Georg Zetzsche. General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond. TACAS 2021

Award Nominations

• Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich and Wolfgang Ahrendt. Deductive Verification of Floating-Point Java Programs in KeY. TACAS 2021
• Elvira Albert, Reiner Hähnle, Alicia Merayo and Dominic Steinhöfel. Certified Abstract Cost Analysis. FASE 2021
• Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham. Run-time Complexity Bounds Using Squeezers. ESOP 2021

EATCS Best Paper Award

• Thomas Neele, Antti Valmari and Tim A.C. Willemse. The inconsistent labelling problem of stutter-preserving partial-order reduction. FoSSaCS 2020

EASST Best Paper Award

• Florian Frohn. A calculus for modular loop acceleration. TACAS 2020

EAPLS Best Paper Award

• Raffi Khatchadourian, Yiming Tang, Mehdi Bagherzadeh and Baishakhi Ray. An empirical study on the use and misuse of Java 8 streams. FASE 2020

Award Nominations

• Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter and Jérémy Thibault. Trace-Relating Compiler Correctness and Secure Compilation. ESOP 2020
• Massimo Benerecetti, Daniele Dell’Erba and Fabio MogaveroCarmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter and Jérémy Thibault. Trace-Relating Compiler Correctness and Secure Compilation. ESOP 2020
• Massimo Benerecetti, Daniele Dell’Erba and Fabio Mogavero. Solving Mean-Payoff Games via Quasi Dominions. TACAS 2020
• Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen and Andreas Pavlogiannis. Optimal and Perfectly Parallel Algorithms for On-demand Data-flow Analysis. ESOP 2020
• Mathieu Huot, Sam Staton and Matthijs Vákár. Correctness of automatic differentiation via diffeologies and categorical gluing. FoSSaCS 2020
• Christof Löding, P. Madhusudan, Adithya Murali and Lucas Peña. A First-Order Logic with Frames. ESOP 2020
• Sreeja S Nair, Gustavo Petri and Marc Shapiro. Proving the safety of highly-available distributed objects. ESOP 2020
• Rong Pan, Qinheping Hu, Rishabh Singh and Loris D’Antoni. Solving Program Sketches with Large Integer Values. ESOP 2020
• Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget and Peter Sewell. ARMv8-A system semantics: instruction fetch in relaxed architectures. ESOP 2020
• Freek Verbeek, Joshua Bockenek and Binoy Ravindran. Highly Automated Formal Proofs over Memory Usage of Assembly Code. TACAS 2020

EATCS Best Paper Award

• Jérémy Dubut. Trees in partial higher dimensional automata. FoSSaCS 2019

EASST Best Paper Award

• Søren Enevoldsen, Kim G. Larsen, Jiří Srba. Abstract dependency graphs and their application to model checking. TACAS 2019

EAPLS Best Paper Award

• Dylan McDermott, Alan Mycroft. Extended call-by-push-value: reasoning about effectful programs and evaluation order. ESOP 2019

Award Nominations

• Martin Brain, Florian Schanda, Youcheng Sun. Building better bit-blasting for floating-point problems. TACAS 2019
• Andrea Corradini, Tobias Heindel, Barbara König, Dennis Nolte,Arend Rensink. Rewriting abstract structures: materialization explained categorically. FoSSaCS 2019
• Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Bernays-Schoenfinkel-Ramsey class of separation logic on arbitrary domains. FoSSaCS 2019
• Lars Fritsche, Jens Kosiol, Andy Schürr, Gabriele Taentzer. Efficient model synchronization by automatically constructed repair processes. FASE 2019
• Rolf Hennicker, Alexandre Madeira, Alexander Knapp. A hybrid dynamic logic for event/data-based systems. FASE 2019
• Marijn Heule, Benjamin Kiesl, Armin Biere. Encoding redundancy for satisfaction-driven clause learning. TACAS 2019

EATCS Best Paper Award

• Sergey Goncharov and Lutz Schröder. Guarded Traced Categories. FoSSaCS 2018

EASST Best Paper Award

• Márton Búr, Gábor Szilágyi, András Vörös and Daniel Varró. Distributed Graph Queries for Runtime Monitoring of Cyber-Physical Systems. FASE 2018

EAPLS Best Paper Award

• Ilya Grishchenko, Matteo Maffei and Clara Schneidewind. A Semantic Framework for the Security Analysis of Ethereum smart contracts. POST 2018

Award Nominations

• Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Christoph Matheja. How Long, O Bayesian Network, Will I Sample Thee? A Program Analysis Perspective on Expected Sampling Times. ESOP 2018
• Randal Bryant. Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. TACAS 2018
• Gabriele Costa, David Basin, Chiara Bodei, Pierpaolo Degano and Letterio Galletta. From Natural Projection to Partial Model Checking and Back. TACAS 2018
• Zinovy Diskin, Harald König and Mark Lawford. Multiple Model Synchronization with Multiary Delta Lenses. FASE 2018
• Marco Eilers, Peter Müller, Samuel Hitz. Modular Product Programs. ESOP 2018
• Guilhem Jaber and Nikos Tzevelekos. A Trace Semantics for System F Parametric Polymorphism. FoSSaCS 2018
• Pierre-Marie Pédrot and Nicolas Tabareau. Failure Is Not an Option: An Exceptional Type Theory. ESOP 2018
• Luigi Santocanale. The Equational Theory of the Natural Join and of Inner Union Is Decidable. FoSSaCS 2018
• Lau Skorstengaard, Dominique Devriese and Lars Birkedal.. Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. ESOP 2018
• Ana Sokolova and Harald Woracek. Proper Semirings and Proper Convex Functors. FoSSaCS 2018
• Daniel Strüber, Sven Peldszus and Jan Jürjens. Taming Multi-Variability of Software Product Line Transformations. FASE 2018
• Alexander J. Summers and Peter Müller. Automating Deductive Verification for Weak-Memory Programs. TACAS 2018

EATCS Best Paper Award

• Sam Staton. Commutative Semantics for Probabilistic Programming. ESOP 2017
• Alex Simpson. Cyclic Arithmetic Is Equivalent to Peano Arithmetic. FoSSaCS 2017
• Stefano Berardi, Makoto Tatsuta. Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System. FoSSaCS 2017

EASST Best Paper Award

• Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule and Isil Dillig. Static Detection of DoS Vulnerabilities in Programs That Use Regular Expressions. TACAS 2017

EAPLS Best Paper Award

• Ryan Culpepper and Andrew Cobb. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. ESOP 2017

Award Nominations

• Parosh Aziz Abdulla, Mohamed Fauzi Atig, Ahmed Bouajjani and Tuan Phong Ngo. Context-Bounded Analysis for POWER. TACAS 2017
• Dimitar Asenov, Balz Guenat, Peter Müller and Martin Otth. Precise Version Control of Trees with Line-Based Version Control Systems. FASE 2017
• Kushel Babel, Vincent Cheval and Steve Kremer. On Communication Models When Verifying Equivalence Properties. POST 2017
• Arthur Blot, Masaki Yamamoto and Tachio Terauchi. Compositional Synthesis of Leakage Resilient Programs. POST 2017
• Michele Boreale. Algebra, Coalgebra, and Minimization in Polynomial Differential Equations. FoSSaCS 2017
• Zheng Cheng and Massimo Tisi. A Deductive Approach for Fault Localization in ATL Model Transformations. FASE 2017
• Samuel Drews and Loris D’Antoni. Learning Symbolic Automata. TACAS 2017
• Erik Krogh Kristensen and Anders Møller. Inference and Evolution of TypeScript Declaration Files. FASE 2017
• Luca Padovani. Context-Free Session Type Inference. ESOP 2017
• Paula Severi. A Light Modality for Recursion. FoSSaCS 2017

EATCS Best Paper Award

• Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Federico Olmedo. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. ESOP 2016
• Neil Ghani, Fredrik Nordvall Forsberg and Alex Simpson. Comprehensive Parametric Polymorphism: Categorical Models and Type Theory. FoSSaCS 2016

EASST Best Paper Award

• Marcus Gerhold and Mariëlle Stoelinga. Model-Based Testing of Probabilistic Systems. FASE 2016
• Veronique Cortier, Antoine Dallon and Stephanie Delaune. Bounding the Number of Agents, for Equivalence Too. POST 2016

EAPLS Best Paper Award

• Daniel Huang and Greg Morrisett. An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages. ESOP 2016

Award Nominations

• Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. Approaching the Coverability Problem Continuously. TACAS 2016
• Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. Family-Based Modeling and Analysis for Probabilistic Systems – Featuring ProFeat. FASE 2016
• Przemysław Daca, Thomas Henzinger, Jan Křetínský and Tatjana Petrov. Faster Statistical Model Checking for Unbounded Temporal Properties. TACAS 2016
• Alexander Faithfull, Jesper Bengtson, Tassi Enrico and Carst Tankink. Coqoon: an IDE for Interactive Proof Development in Coq. TACAS 2016
• Gudmund Grov and Vytautas Tumas. Tactics for the Dafny Program Verifier. TACAS 2016
• P. Madhusudan, Daniel Neider and Shambwaditya Saha. Synthesizing Piece-wise Functions by Learning Classifiers. TACAS 2016
• Antoine Miné, Jason Breck and Thomas Reps. An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs. ESOP 2016
• Jian Xiong Shao, Yu Qin and Dengguo Feng. Computational Soundness Results for Stateful Applied pi Calculus. POST 2016
• Daniel Strüber, Julia Rubin, Thorsten Arendt, Marsha Chechik, Gabriele Taentzer and Jennifer Plöger. RuleMerger: Automatic Construction of Variability-Based Model Transformation Rules. FASE 2016

EATCS Best Paper Award

• Konstantinos Mamouras. Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism. FoSSaCS 2015

EASST Best Paper Award

• Mirco Giacobbe, Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Tiago Paixão, and Tatjana Petrov. Model checking Gene Regulatory Networks. TACAS 2015

EAPLS Best Paper Award

• Pierre Neron, Andrew Tolmach, Eelco Visser, and Guido Wachsmuth. A Theory of Name Resolution. ESOP 2015

Award Nominations

• Delphine Demange, David Pichardie, and Leo Stefanesco. Verifying Fast and Sparse SSA-based Optimizations in Coq. CC 2015
• Alain Darte and Alexandre Isoard. Exact and Approximated Data-Reuse Optimizations for Tiling with Parametric Sizes. CC 2015
• Nicholas Allen, Bernhard Scholz, and Padmanabhan Krishnan. Staged Points-to Analysis for Large Code Bases. CC 2015
• Radu Calinescu, Simos Gerasimou, and Alec Banks. Self-Adaptive Software with Decentralised Control Loops. FASE 2015
• S.C.C. Blom, S. Darabi, and M. Huisman. Verification of Loop Parallelisations. FASE 2015
• Timos Antonopoulos, Paul Hunter, Shahab Raza, and James Worrell. Three Variables Suffice for Real-Time Logic. FoSSaCS 2015
• Binh Thanh Nguyen and Christoph Sprenger. Abstractions for Security Protocol Verification. POST 2015
• Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. Approximate Counting in SMT and Value Estimation for Probabilistic Programs. TACAS 2015

EATCS Best Paper Award

• Christel Baier, Joachim Klein, Sascha Klueppelholz, Steffen Märcker. Computing conditional probabilities in Markovian models efficiently. TACAS 2014
• Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada. Unsafe order-2 tree languages are context-sensitive. FoSSaCS

EASST Best Paper Award

• Christian Von Essen, Dimitra Giannakopoulou. Analyzing the next generation airborne collision avoidance system. TACAS 2014

EAPLS Best Paper Award

• Justin Slepak, Olin Shivers, Panagiotis Manolios. An array-oriented language with static rank polymorphism. ESOP

Award Nominations

• Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martin Ochoa. Leakage resilience against concurrent cache attacks. POST 2014
• Marcello Maria Bersani, Domenico Bianculli, Carlo Ghezzi, Srdjan Krstic, Pierluigi San Pietro. SMT-based checking of SOLOIST over sparse traces. FASE 2014
• Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta. Formal design of fault detection and identification components with temporal epistemic logic. TACAS 2014
• Ravi Mangal, Mayur Naik, Hongseok Yang. A correspondence between two approaches to interprocedural analysis in the presence of join. ESOP 2014
• Annabelle McIver, Carroll Morgan, Geoffrey Smith, Barbara Espinoza, Larissa Meinicke. Abstract channels and their robust information-leakage ordering. POST 2014
• Luca Padovani. Type reconstruction for the linear π-calculus with composite and equi-recursive types. FOSSACS
• Perdita Stevens. Bidirectionally tolerating inconsistency: partial transformations. FASE 2014

EATCS Best Paper Award

• Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, Matteo Maffei. Logical foundations of secure resource management in protocol implementations. POST 2013

EASST Best Paper Award

• Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík, Bengt Jonsson, Ahmed Rezine. An integrated specification and verification technique for highly concurrent data structures. TACAS 2013

EAPLS Best Paper Award

• Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, Claudio Russo. Deriving probability density functions from probabilistic functional programs. TACAS 2013

Springer’s Best Student Paper Award

• Grigori Fedyukovich, Ondrej Sery, Natasha Sharygina. eVolCheck: incremental upgrade checker for C. TACAS 2013
• Robbert Krebbers, Freek Wiedijk. Separation logic for non-local control flow and block scope variables. FoSSaCS 2013
• Shin-ya Katsumata, Tetsuya Sato. Preorders on monads and coalgebraic simulations. FoSSaCS 2013

Award Nominations

• Faris Abou-Saleh, Dirk Pattinson. Comodels and effects in mathematical operational semantics. FoSSaCS 2013
• Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare. On-the-fly exact computation of bisimilarity distances. TACAS 2013
• Arbi Bouchoucha, Houari Sahraoui, Pierre L’Ecuyer. Towards understanding the behavior of classes Using probabilistic models of program inputs. FASE 2013
• Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer. Interleaving and lock-step semantics for analysis and verification of GPU kernels. ESOP 2013
• Fredrik Dahlqvist, Dirk Pattinson. Some Sahlqvist completeness results for coalgebraic modal logics. FoSSaCS 2013
• Pietro Di Gianantonio, Abbas Edalat. A language for differentiable functions. FoSSaCS 2013
• Alexey Gotsman, Noam Rinetzky, Hongseok Yang. Verifying concurrent memory reclamation algorithms with Grace. ESOP 2013
• Radha Jagadeesan, Gustavo Petri, Corin Pitcher, James Riely. Quarantining weakness. ESOP 2013
• Nuno Macedo, Alcino Cunha. Implementing QVT-R bidirectional model transformations using Alloy. FASE 2013

EATCS Best Paper Award

• Sebastian Preugschat, Thomas Wilke. Effective characterizations of simple fragments of temporal logic using prophetic automata. FoSSaCS 2012

EASST Best Paper Award

• Aharon Abadi, Ran Ettinger, Yishai A. Feldman. Fine slicing – theory and applications for computation extraction. FASE 2012
• Fu Song, Tayssir Touili. Pushdown model checking for malware detection. TACAS 2012

EAPLS Best Paper Award

• Zhenyue Long, Georgel Calin, Rupak Majumdar, Roland Meyer. Language-theoretic abstraction refinement, FASE 2012

Award Nominations

• Danel Ahman, James Chapman, Tarmo Uustalu. When Is a container a comonad? FoSSaCS 2012
• Matteo Centenaro, Riccardo Focardi, Flaminia L. Luccio. Type-based analysis of PKCS#11 key management. POST 2012
• Pierre-Malo Deniélou, Nobuko Yoshida. Multiparty session types meet communicating automata. ESOP 2012
• Paul Downen, Zena M. Ariola. A systematic approach to delimited control with multiple prompts. ESOP 2012
• Jason Franklin, Sagar Chaki, Anupam Datta, Jonathan M. McCune, Amit Vasudevan. Parametric verification of address space separation. POST 2012
• Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur, Rahul Mangharam. Modeling and verification of a dual chamber implantable pacemaker. TACAS 2012
• Frédéric Lang, Radu Mateescu. Partial model checking using networks of labelled transition systems and Boolean equation systems. TACAS 2012
• Miriam Paiola, Bruno Blanchet. Verification of security protocols with lists: from length one to unbounded length. POST 2012

EATCS Best Paper Award

• Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala. Canonized rewriting and ground AC-completion modulo Shostak theories. TACAS 2011

EASST Best Paper Award

• Alessandro Cimatti, Iman Narasamdya, Marco Roveri. Boosting lazy abstraction for SystemC with partial order reduction. TACAS 2011

EAPLS Best Paper Award

• Dominik Grewe, Michael O’Boyle. A static task partitionic approach for heterogeneous systems using OpenGL. CC 2011

Springer’s Best Student Paper Award

• Matteo Mio. Probabilistic modal mu-calculus with independent product. FoSSaCS 2011
• Sebastian Buchwald, Andreas Zwinkau, Thomas Bersch. SSA-based register allocation with PBQP. CC 2011

Award Nominations

• Patrick Cousot, Radhia Cousot, Laurent Mauborgne. The reduced product of abstract domains and the combination of decision procedures. FoSSaCS 2011
• José Luiz Fiadeiro, Antónia Lopes. An interface theory for service-oriented design. FASE 2011
• Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani. Efficient interpolant generation in satisfiability modulo linear integer algebra. TACAS 2011
• Huiqing Li, Simon Thompson. Incremental code clone detection and elimination for Erlang programs. FASE 2011
• Mieke Massink, Diego Latella, Andrea Bracciali, Jane Hillston. Modelling non-linear crowd dynamics in Bio-PEPA. FASE 2011
• Yaron Velner, Alexander Rabinovich. Church synthesis problem for noisy input. FoSSaCS 2011